docs(mosaic): preserve static nested offline geometry and review evidence

This commit is contained in:
fy59 2026-10-13 16:25:56 +02:00
parent 899c007c37
commit bbd7da2403
23 changed files with 2990 additions and 0 deletions

View file

@ -4,6 +4,8 @@
### STEP20C experimental evidence
- Local offline nested geometry/fixture review protocol: separate SHM, assigned/rendered, scene, XDG and PNG spaces; exhaustive assertion/source/test register and independent review required. No graphical launch authorized; final offline verdict INCONCLUSIVE.
- Preserved static nested-grab fixture failure: sole unchanged-binary run confirms identity/output/camera/tiled clip and exact whole-H2 pre-popup references, then fails before any click/grab on a native-SHM versus painted-height assertion. INCONCLUSIVE / UNDECIDED; additional IPC-y/titlebar assumption invalid, offline assertion audit insufficient. Raw runner exit1 and compositor exit0 retained; popup/standard gates NOT TESTED, no retry/build/production change. Historical runner and sealed artifacts preserved.
- Preserved independent static RGB/input/standard retest: corrected shared predicate and real replay pass; exact whole-H2 RGB, H1 retained/H2 forbidden pixels, real target/reference clicks and targeted splith clip removal/input pass. FEASIBLE for this matrix. Terminal exit IPC makes runner exit 1 after measured gates and compositor exit 0; raw failure retained and offline diagnosis passes. No new compositor/library build or production change.
@ -72,3 +74,17 @@
- Ordinary SwayFX remains separately installed and independently updatable; no automatic session replacement.
- Multi-output clipping, multiple runtime rows, camera animation, Session V2 restore, final cell sizing, and daily-driver qualification remain open. See [known limitations](docs/KNOWN_LIMITATIONS.md).
### Preserved offline nested geometry gate — EXPERIMENTAL / INCONCLUSIVE
- Replayed true static failure SHM/configure/destination/titlebar/paint data and
nine preserved private/control popup campaigns, without any graphical run.
- Prepared typed shared geometry, actual-configure/lifecycle/input validators,
exhaustive145 historical assertions/2288 AST-site register and195 passing
offline tests; compiled only three C17 client utilities, never executed.
- Preserved the independent deep review and bounded repair/delta review:
input correlation and terminal IPC evidence fixes accepted, readiness receipt
semantic-completeness defect remains CORRECTION_REQUIRED. No READY claim.
- Preserved the [geometry gate](docs/design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md)
and experimental source fixture with its historical INCONCLUSIVE verdict; STEP20C NEXT, architecture UNDECIDED and
production multi-output NOT YET SUPPORTED. No production/package/UX change.

View file

@ -443,3 +443,14 @@ are NOT TESTED in this campaign. No algorithm/production/UX/package change or
retry; budget exhausted. Correct/replay geometry predicates offline before a
separately authorized fresh static popup gate. Historical failure evidence is frozen;
STEP20C NEXT, production multi-output NOT YET SUPPORTED.
The preserved [static nested geometry replay gate](design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md)
is EXPERIMENTAL / INCONCLUSIVE. True SHM/configure/paint geometry and nine
historical popup cases were replayed;145 historical asserts and2288 current AST
sites are classified, with partial executed coverage explicit.195 offline tests
pass, but independent review retains CORRECTION_REQUIRED: the readiness
aggregator accepts semantically incomplete proof records. Input correlation and
terminal-code repairs are accepted; no readiness or new static popup result.
No graphical run or execution reservation occurred. Close the residual offline
receipt-validation gate before proposing runtime. Architecture UNDECIDED;
STEP20C NEXT; production multi-output NOT YET SUPPORTED.

View file

@ -384,3 +384,14 @@ are NOT TESTED in this campaign. No algorithm/production/UX/package change or
retry; budget exhausted. Correct/replay geometry predicates offline before a
separately authorized fresh static popup gate. Historical failure evidence is frozen;
STEP20C NEXT, production multi-output NOT YET SUPPORTED.
The preserved [static nested geometry replay gate](design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md)
is EXPERIMENTAL / INCONCLUSIVE. True SHM/configure/paint geometry and nine
historical popup cases were replayed;145 historical asserts and2288 current AST
sites are classified, with partial executed coverage explicit.195 offline tests
pass, but independent review retains CORRECTION_REQUIRED: the readiness
aggregator accepts semantically incomplete proof records. Input correlation and
terminal-code repairs are accepted; no readiness or new static popup result.
No graphical run or execution reservation occurred. Close the residual offline
receipt-validation gate before proposing runtime. Architecture UNDECIDED;
STEP20C NEXT; production multi-output NOT YET SUPPORTED.

View file

@ -302,3 +302,14 @@ are NOT TESTED in this campaign. No algorithm/production/UX/package change or
retry; budget exhausted. Correct/replay geometry predicates offline before a
separately authorized fresh static popup gate. Historical failure evidence is frozen;
STEP20C NEXT, production multi-output NOT YET SUPPORTED.
The preserved [static nested geometry replay gate](design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md)
is EXPERIMENTAL / INCONCLUSIVE. True SHM/configure/paint geometry and nine
historical popup cases were replayed;145 historical asserts and2288 current AST
sites are classified, with partial executed coverage explicit.195 offline tests
pass, but independent review retains CORRECTION_REQUIRED: the readiness
aggregator accepts semantically incomplete proof records. Input correlation and
terminal-code repairs are accepted; no readiness or new static popup result.
No graphical run or execution reservation occurred. Close the residual offline
receipt-validation gate before proposing runtime. Architecture UNDECIDED;
STEP20C NEXT; production multi-output NOT YET SUPPORTED.

View file

@ -388,3 +388,14 @@ are NOT TESTED in this campaign. No algorithm/production/UX/package change or
retry; budget exhausted. Correct/replay geometry predicates offline before a
separately authorized fresh static popup gate. Historical failure evidence is frozen;
STEP20C NEXT, production multi-output NOT YET SUPPORTED.
The preserved [static nested geometry replay gate](design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md)
is EXPERIMENTAL / INCONCLUSIVE. True SHM/configure/paint geometry and nine
historical popup cases were replayed;145 historical asserts and2288 current AST
sites are classified, with partial executed coverage explicit.195 offline tests
pass, but independent review retains CORRECTION_REQUIRED: the readiness
aggregator accepts semantically incomplete proof records. Input correlation and
terminal-code repairs are accepted; no readiness or new static popup result.
No graphical run or execution reservation occurred. Close the residual offline
receipt-validation gate before proposing runtime. Architecture UNDECIDED;
STEP20C NEXT; production multi-output NOT YET SUPPORTED.

View file

@ -0,0 +1,459 @@
# STEP20C static nested geometry replay and offline fixture review
**EXPERIMENTAL / INCONCLUSIVE offline gate. Runtime NOT TESTED.** This protocol is
written before changing the corrected fixture. Phase A published the historical
INCONCLUSIVE failure in commit899c007c37beac03a337ba58ead4326ea8db8878,
verified directly on both remotes with clean worktree. This new phase stays
local, uncommitted and unpublished. **No compositor or graphical client may
be launched, no socket/PNG/input/grab/camera/run reservation created.**
Canonical [architecture](../ARCHITECTURE.md), [UX](../UX.md),
[limitations](../KNOWN_LIMITATIONS.md) and [roadmap](../ROADMAP.md) govern.
STEP20A DONE, STEP20B EXPERIMENTAL, STEP20C NEXT, STEP20D–G PLANNED;
production multi-output NOT YET SUPPORTED, architectural conclusion UNDECIDED.
## Errors and authoritative observations
The [frozen historical failure](STEP20C_STATIC_NESTED_VALID_GRAB_PROBE.md)
retains native SHM420×320, configure636×573, SceneFX destination636×573,
owner applied scene(-320,0,640,600), IPC window_rect(2,0,636,573), effective
25px titlebar and blue paint global[-318,0)×[25,598), PNG local
[482,25,800,598),182214 pixels. Applied scroll160 and global clip
[-800,0)×[0,600) pass. Runner exit1, terminal IPC1, compositor0; zero popup/grab.
Do not alter its LAB, ledgers, manifests or source fixtures. Reproduce and
reject native-height=paint-height and scene.y+window_rect.y=paint.y assumptions.
## Explicit geometry contract
Separate immutable logical structures carry provenance and coordinate-space
tags: NativeSHM (buffer identity, source pixels/format/stride), XDG configure
(role-local coordinates and ACK), AppliedContent (current assignment and
state trace), SceneGlobal (node translation and content/decor/view offsets),
PopupLocal (parent XDG geometry), ViewportGlobal (applied inherited clip),
OutputPNG (origin/scale/transform and RGB paint). Rectangles are half-open.
Conversions reject wrong spaces, origin, ownership, pending-as-applied,
unmeasured scaling/transform, identity mismatches and unchecked bounds.
The future runner and replay use the SAME conversion/validation functions.
Pinned retained source: swayfx-mosaic-static-runtime-hm5kbdkt/{mosaic-source,
scene-source,wlroots-source}. SwayFX output_configure_scene sets tiled buffer
destination from animation_state.current_content_width/height. Transaction
arrangement subtracts borders/titlebar and positions view scene by border_left/
border_top. IPC window_rect describes assigned content with titlebar-dependent
y=0; it is not a scene position or native-buffer size. Applied traces, source
arrangement, natural geometry and captured paint must agree separately. PNG
identity never substitutes for native committed-buffer identity.
Root popup scene wrapper is in root->layers.popup and placed at the applied
view content tree origin; B is beneath A's XDG scene tree. output_configure_scene
inherits closest_con only from container descriptors; globally parented popup
branches do not inherit tiled dest_size resizing. Verify this specific path,
not an assumption that all popup dimensions equal toplevel destination.
SceneFX tree-local clips intersect ancestors for render and hit testing. Root
popup clip is derived from current owning workspace's applied tiling viewport,
converted to root-local, with owner visibility guard. Standard layout clears
root/tiled clips; B's inherited boundary follows its parent. Existing traces
have limited root/owner identity: select only a bounded chain/window and require
unique correlation; ambiguity stops measurement, never arbitrary last-trace use.
## XDG positioner and protocol
Historical client and new placement patch are byte-identical to frozen inputs.
A anchor(100,80),350×170; B anchor(100,60),300×130; 1×1 anchor rectangles inside
parent geometry; anchor TOP_LEFT,gravity BOTTOM_RIGHT, no explicit constraint
adjustment. Pinned wlroots allocates rules with calloc, default flags0; flip,
slide,resize each require matching nonzero bits. Unconstrain is still called
but flags0 do not enable adjustment. Read actual configure/ACK/map each time;
requested coordinates are source-backed predictions, never runtime evidence.
For applied content(-318,25), predicted A[-218,132)×[105,275),
B[-118,182)×[165,295). If either actual popup does not cross, report NOT EXERCISED.
B.parent is A.xdg_surface with grabbing mapped A. Both grabs originate from
separate real left-press serials; WAYLAND_DEBUG independently confirms requests,
bufferless commit/configure/ACK/attach/map and child-first destruction.
## Offline evidence and exhaustive assertion register
Read the historical failed LAB and, if available, the preserved nested LAB
/tmp/swayfx-mosaic-nested-grab-If8ofeUu. Replay at least b_cross, both_cross,
standard return with mapped A/B, and valid-grab dismissal. Read actual XDG
objects/serials/configures/ACK/map, IPC camera/output/layout, root clip logs,
PNG colors/occlusions/intersections and pointer button/local coordinates.
Unavailable evidence must say NOT AVAILABLE / NOT REPLAYED. Future execution
must use versioned sources and discovered IDs, never depend on temporary old LABs.
Automatically enumerate ALL assertions, Defect raises, checked validation calls,
size/geometry/identity/focus/serial/conversion conditions, terminal and cleanup
branches in the four historical modules and corrected proposed runner/model.
Each record contains file/line/function/stage/domain/invariant/source support,
replay possibility, executed positive/negative test IDs, runtime dependency and
retain/correct/replace/remove decision with justification. No unclassified
record. Operational pure-error branches may use labelled synthetic cases;
unexecuted runtime facts remain NOT TESTED. A broad synthetic test label is not
proof that each assertion has been challenged. Coverage is checked against AST
and actual test receipts; source inventory and checker freshness are required.
Required negative cases include both historical errors, wrong output/PNG origin,
assignment, workspace/owner, old camera, local/global clip, buffer identity,
pending-as-applied, scale/transform, missing/invalid serial/parent/ACK/map,
clip/occlusion errors, reused E2 identity, standard stale origin, dismissal
confused with invisible input, and terminal transport with incomplete measures.
Client-only C17 -Werror compile/syntax and generated-protocol checks are allowed;
no execution of graphical clients, compositor or new library build.
## Future ordered runner — prepared only
A future ticket must independently authorize one headless run and its durable
ledger. This ticket creates no execution budget. The runner must refuse without
explicit future authorization/readiness and fresh registered LAB; historical
budget paths cannot be used. Proposed maxima: compositor1, chains2, grabs4,
camera2(one/chain),Mosaic→splith1,clicks9,PNG16,positions24,duration150s.
Client-only preparation can compile fixtures; no Mosaic/SceneFX build.
Discover private sockets, binary/maps, actual outputs, reference ID/PID,
Mosaic owner/workspace/focus and applied geometry before measurement. Establish
H1/focus/camera and two exact full H2 references before grabs. E1 opens A/B with
real buttons, qualifies both actual crossings/colors/root inherited clipping,
visible B input then forbidden B input and normal outside dismissal. Close E1
normally. E2 is new client/IDs/serials; reopen under Mosaic, keep popups mapped
through targeted splith, remeasure owner/content/popups/root clip and H2 colors,
click standard B, explicitly close B, click surviving A, close normally and
require final exact H2. Planned8 clicks/15PNG; fail consumption never refunded.
Native SHM dimensions are correlated to rendered destination and visible
intersection, not required equal. Titlebar/content origin is derived from
applied source arrangement, independently checked by paint. Actual popup
configure and fresh owner origin drive geometry and pointer conversions;
popup painting accounts for occlusion, viewport and output. No blind reuse of
Mosaic origin for splith. No premature exterior click in E2.
Terminal IPC keeps actual stdout/stderr/code. Exception for lost transport
reply is allowed only after all measures, actual handled exit, compositor0,
no protocol/crash/timeout/rescue and all owned processes reaped. Incomplete
measurements remain failure despite clean shutdown. Capture/frame/native-buffer
identity, atomic generation and full damage cannot be established offline.
## Independent review and readiness rules
One independent configured Astra final-reviewer receives contracts, source delta,
assertion inventory and evidence, searches the entire E1/E2/standard/cleanup
path, and writes independent-review.md with ACCEPTED, CORRECTION_REQUIRED and
NOT PROVEN findings. Author addresses every finding and runs bounded correction
validation. No reviewer availability means no ready claim. No broad re-review
loop; one bounded repair chain and delta review if required.
Markers may be PASS only after execution: STATIC_NESTED_SHM_RENDER_GEOMETRY_REPLAY,
STATIC_NESTED_XDG_GEOMETRY_AUDIT, STATIC_NESTED_ASSERTION_COVERAGE,
STATIC_NESTED_OFFLINE_REGRESSIONS, STATIC_NESTED_INDEPENDENT_REVIEW.
All PASS yields SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE=
READY_FOR_NEW_RUNTIME (fixture only, no static popup success). Unresolved
necessary model/fixture evidence gives INCONCLUSIVE; proven structural invalidity
outside allowed fixture correction gives BLOCKED. Architectural conclusion
remains UNDECIDED for STEP20C.
Retain exact sources/source excerpts or hashes, client/protocol provenance,
replay receipts, register/coverage/positive/negative/review/readiness/summary
JSON and once-sealed SHA256 manifests in an offline LAB outside Git. No binary,
PNG/build/socket/large log in Git. Synchronize report/fixture README/canonical
architecture,limitations,roadmap,index,changelog; phase B never committed/pushed.
## Author validation completed before independent review
Offline LAB `/home/fy59/swayfx-mosaic-static-nested-geometry-replay-a56csvoo`.
No runtime ledger, compositor, client execution, socket, PNG capture, pointer,
grab or camera operation. Author's final suite:131 tests PASS in30.588s;
9 actual historical popup cases replayed, three client-only C17 -Werror builds
and generated protocol byte identity PASS. The initial reference syntax attempt
failed because its included saved-client.c dependency had not been copied; copy
the exact versioned dependency, change no C source, and all three checks pass.
The true failed snapshot recovers SHM420×320, configure636×573, assigned rendered
destination636×573, scene(-320,0,640,600), window(2,0,636,573), titlebar25,
origin(-318,25), visible PNG bbox[482,25,800,598),182214 pixels,scroll160,
viewport[-800,0)×[0,600). Initial configure0×0/ACK20/nativeMAP and subsequent
636×573/ACK21/no replacement buffer remain distinct. The two historical errors
are rejected by shared typed functions. PNG/native-frame identity stays NOT PROVEN.
Pinned source audit verifies1397/1397 retained source entries and658/658 old
nested artifacts. Seventeen source contract items have exact copies/hashes,
functions and excerpts in LAB. SceneFX destination and native input bounds are
separate: opening click must fit actual blue paint AND native input region.
Popup-global branches retain their own native/current configured sizes.
Default positioner flags0 disables flip/slide/resize, despite unconstrain calls.
Actual configured geometry still drives measurement; predicted static A/B are
not a runtime result. Root trace selection is restricted to the current chain,
owner origin and observation window; ambiguity is a fixture stop. Standard
origin is freshly computed. Dismissal never substitutes for invisible button.
| Actual historical case | Configured global geometry | Actual sampled RGB/input/lifecycle |
| --- | --- | --- |
| Private b_cross | origin(242,25), A(442,105,300,170), B(662,165,300,130) | grabs55/60; H1 A42200/B17940,H2 zero; visibleB65/66; exterior B→A done/destruction |
| Private both_cross | origin(242,25), A(592,105,350,170), B(752,165,300,130) | grabs55/60; H1 A30080/B6240,H2 zero; separate A/B buttons; exterior dismissal |
| Private toggle | Mosaic origin(242,25)→standard(202,25), A(402,105,300,170), B(622,165,300,130) in standard | same mapped objects, no prior popup_done; H2 B15860; B69/70 delivered |
| Private outside | A(292,105,250,170),B(312,165,170,130) | grabs55/60; outside ordinary client button, B then A popup_done, child-first destroy |
| Control b_cross | origin(202,25),A(402,105,300,170),B(622,165,300,130) | grabs61/66; H2 B15860 and actual B buttons |
| Control both_cross | origin(202,25),A(552,105,350,170),B(712,165,300,130) | grabs61/66; H2 A6120/B27560, actual A/B buttons |
| Control outside | A(252,105,250,170),B(272,165,170,130) | grabs59/64; topmost-first done and destruction |
| Private/control close_b-visible | actual source/log configure and masks replayed | explicit B destruction, A survives and receives right buttons; no erroneous left-click reopening |
Historical standard root clear has source/pixel/input evidence; that old binary
has no explicit clip-clear trace, so direct node-state proof is NOT PROVEN.
Future static runner must use its existing PI_POPUP trace. Old origins without
PI_OWNER are explicitly corroborated from clip + source/IPC + paint/pointer,
not presented as an independently sampled current trace. These replays validate
fixture methods; no new static popup result follows.
Register:2114 sites, including every145 historical assertions;295 sites have
executed positive+negative receipts,568 positive-only and1245 unexecuted sites
explicitly classified. This is NOT2114 runtime facts. Source/AST hashes, exact
line or named-contract receipts reject missing/stale/duplicate/unclassified or
fabricated support. Core pure model/provenance/conversion/authorization/ledger/
pixel guards are tested; runtime-only facts and retired historical code remain
identified separately. Author checker reports0 unresolved pure invariants.
The independent review must assess whether these classifications and coverage
are justified; no independent PASS or READY is claimed before that review.
Corrections cover buffer/destination/titlebar, pending/applied provenance,
output-to-PNG transforms, actual rather than requested popup configures, B
occlusion/output/inherited viewport, native input bounds, root/owner observation
window, new E2 identities/serials, fresh standard generation, lifecycle and
terminal codes. Client placement remains the exact e0e87f… patch. Future runner
requires distinct future authorization and accepted readiness before any debit,
process, runtime or socket creation; current/historical LABs are rejected.
It depends on versioned sources/protocol hashes, not old temporary evidence.
Author markers at this stage: SHM replay PASS, XDG audit PASS offline,
assertion coverage PASS inventory/classification/freshness/core guard scope,
offline regressions PASS; independent review NOT RUN. Readiness INCONCLUSIVE
pending independent review. Architecture UNDECIDED; new runtime NOT TESTED.
## Independent deep review — corrections required
The configured independent final-reviewer (GPT-6-Astra/high, isolated,
read-only) completed one deep audit. Its exact report is retained as
LAB/independent-review.md and its initial structured findings as
results/independent-review-initial.json. The reviewer independently reran131
tests PASS (8.467s, replay writes neutralized), verified all145 historical
assertions among2114 AST sites and the17 pinned contract hashes. This does not
constitute readiness acceptance: three controlled in-memory reproductions
established blocking validator defects.
- R01: callback/injection logs were retained without numerical pairing;
x=99999 callbacks still passed all9 replays. The dismissal replay supplied an
empty button list, accepting an injected invisible B press. Correct actual
phase/geometry/input pairing and pass real relevant buttons, with corruption
regressions; never modify historical logs or claim unavailable attribution.
- R02: readiness ignored failed rendered/source/coverage evidence and hardcoded
XDG/coverage PASS. A synthetic accepted review could yield READY with a failed
SHM marker. Aggregate all effective fresh mandatory gates and independently
degrade each input in tests of the same production aggregator.
- R03: obtaining IPC code7 and then a compositor wait timeout lost the IPC code
in the generic exception receipt. Preserve code/streams immediately before
waiting, append compositor failure separately and retain scientific failure.
The reviewer accepted typed geometry/native input/occlusion, source XDG/scene
contracts, complete inventory within its stated partial execution scope and
future E1/E2/resource order. New runtime/full frame/atomic generation/wider
matrices remain NOT PROVEN/FUTURE_SCOPE, not reasons to run graphics here.
The three blockers require one bounded offline repair chain and a delta review.
No second broad final audit or new graphical campaign is authorized. All
readiness statuses remain INCONCLUSIVE until corrections are verified and
independently accepted. Earlier suite PASS and0 unresolved-core counters are
preserved as their actual results, not promoted to full protocol qualification.
## Bounded offline repairs implemented — acceptance pending
The resolver changed only new replay/write_results/run/predicates/tests/assertions
and fixture README. Initial independent report and initial structured findings
remain byte-identical; final-review-repair.json records root causes, repairs and
actual test outcomes. No historical evidence, production, contract or runtime
budget is modified.
R01 now pairs wire and callback coordinates with action identity/time, real
surface/parent, lifecycle phase and actual configured rectangles, using the
same pointer_local function as future runtime. It handles A's automatic map
retarget, unchanged-position clicks, software motion after layout and fresh
standard origin. Relevant actual forbidden-action buttons reach dismissal;
legitimate earlier visible popup buttons are retained separately. Unidentifiable
old events are labelled NOT AVAILABLE / NOT REPLAYED, never silently promoted.
Corrupted callback/wire coordinates, recipient, extra invisible button and order
are rejected against unmodified archive inputs.
R02 uses one shared aggregator for real results and tests. The repair intended
to require all mandatory geometry/XDG/source/provenance/C17/replay/register/core/
test evidence complete and fresh; the final delta review below proves the
semantic-completeness requirement remains unsatisfied; source_delta/evidence_sha256 bindings must match independent
acceptance. Missing/failed/stale inputs or stale acceptance block readiness.
All marker values are exact PASS/INCONCLUSIVE with separate marker_scope.
Synthetic accepted review in negative/positive tests is memory-only; real
initial review remains CORRECTION_REQUIRED.
R03 uses terminal_exchange in runner and mocks: IPC code/stdout/stderr are stored
before compositor wait. IPC7 then TimeoutExpired retains7 and streams plus a
separate compositor error; scientific result remains false. No obtained code on
invocation error stays explicit null. IPC1 may be separately qualified only
with completed measures, handled clean compositor0 and no crash/protocol/rescue.
Author repair validation:195 tests PASS,32.276s; nine historical replays PASS;
register2288 sites including145 historical assertions,361 positive+negative,
676 positive-only,6 negative-only,1245 unexecuted, core PASS. These are execution
receipts for their limited offline scope, not2288 graphical observations.
A first expanded suite failed because its synthetic positive aggregation
snapshot read stale receipts during editing; snapshot isolation was corrected
and final tests pass. Compilation dependency and AST-key preparation incidents
are likewise preserved. An independent tester and bounded reviewer must still
verify this final delta before READY; no second broad deep audit is performed.
## Final bounded review and disposition — INCONCLUSIVE
Independent tester (GPT-6-Luna/low, isolated) reran the actual offline sequence:
replay,195 tests with0 failures,register generation,register --check,writer.
All commands exit0. AST14 Python files, README shell syntax, diff check,
310 protected paths, immutable24/30/96 historical manifest entries and original
review hashes pass. No new PNG/socket/runtime budget exists.
Independent delta reviewer (GPT-6.1-Sol/medium, isolated, read-only) examined
R01–R03, ran65 targeted tests PASS (4.299s), replayed9 cases with writes disabled
and verified17 source/15 proof bindings. R01 and R03 are RESOLVED. **R02 remains
CORRECTION_REQUIRED / BLOCKING for readiness**, not a demonstrated compositor
or architectural defect. LAB/bounded-review.md and results/bounded-review.json
retain the finding; original Astra report/JSON remain immutable. The parent
independently reproduced all three principal counterexamples with the actual
aggregate and in-memory snapshots, results/parent-R02-reproduction.json:
| Effective mandatory evidence removed | Actual wrong synthetic decision |
| --- | --- |
| Historical input correlation reduced to a bare PASS label | READY, no blocker |
| Rendered content/bbox/count/intersection set to null | READY, no blocker |
| Root popup records replaced by nine empty objects | READY, no blocker |
The reviewer additionally removed protocol/configured/button/callback/injection
and available standard/close/dismissal facts in b_cross,toggle,close_b cases;
all still produced synthetic READY. No acceptance was signed or persisted.
The true LAB remains INCONCLUSIVE because its review is not ACCEPTED.
The existing writer's four technical PASS labels are retained as **raw calculated
results with limited scope**. Their ability to certify complete proof is not
accepted. Counting an AST site or passing195 existing tests cannot override
these executed negative counterexamples.
| Final assessed gate | Result and scope |
| --- | --- |
| STATIC_NESTED_SHM_RENDER_GEOMETRY_REPLAY | PASS — true snapshot/PNG/SHM/destination replay |
| STATIC_NESTED_XDG_GEOMETRY_AUDIT | PASS — pinned source and sampled historical protocol/geometry only |
| STATIC_NESTED_ASSERTION_COVERAGE | PASS — current exhaustive inventory/classification/freshness; partial executed semantic coverage |
| STATIC_NESTED_OFFLINE_REGRESSIONS | INCONCLUSIVE —195 existing tests PASS, semantic deletion/null counterexamples expose an uncovered validator defect |
| STATIC_NESTED_INDEPENDENT_REVIEW | INCONCLUSIVE — CORRECTION_REQUIRED, no acceptance |
`SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE=INCONCLUSIVE`.
Architecture UNDECIDED; no new static popup is qualified. All historical static
popup/grab/input/standard cells remain NOT TESTED. Runtime runner is prepared
but unexecuted and **NOT READY**. Its authorization guard refuses this ticket,
current/historical LABs and unaccepted readiness. No runtime ledger is created.
The single deep final review and its bounded repair/delta review chain are
complete. A material readiness defect survives that chain. Stop repair here,
retain the failure, and request a separately scoped **offline-only** follow-up
for aggregate's effective receipt-content validation and shared-function negative
regressions. This is smaller than any graphical gate. Only after an independently
accepted offline gate could a later distinct ticket authorize one run; nothing
in this report authorizes execution or makes a reservation.
## Required geometry and protocol answers
1. SHM420×320 remains the client's native submission. SwayFX configures636×573
from the tiled content assignment and SceneFX dest_size scales rendering;
the client ACKs but does not replace its original buffer. Native input bounds
are distinct from destination rendering.
2. Applied owner scene(-320,0), left border2 and effective top titlebar25 place
content at(-318,25). IPC window_rect.y=0 alone omits that translation.
3. IPC window_rect/content assignment derives from pending fields; natural
geometry describes native XDG size. Applied PI_OWNER/PI_MOSAIC traces, snapshot
timing and paint correlate actual state; do not label pending rects applied.
4. Translate content/root/global scene explicitly, intersect global viewport
and output, then subtract output origin(-800,0) at measured scale1/normal.
Global(-318,25) becomes PNG(482,25); clipped right edge0 becomes PNG800.
5. Both erroneous assumptions are reproduced and rejected in shared model
negatives using true geometry. The additional aggregator defect is also
reproduced; it is not a geometry failure.
6. All145 historical asserts and current runner/helper sites are inventoried:
2288 sites,361 positive+negative,676 positive-only,6 negative-only,1245
unexecuted explicitly classified. Inventory is not complete branch proof.
7. New applied output/focus/owner/camera/buffer/clip/actual popup configure/map/
crossing/input/dismissal/standard/cleanup and exact rendering remain runtime
observations. Native frame identity and atomic generation are NOT PROVEN.
8. Pinned calloc default constraint flags0 disables flip/slide/resize adjustment
in this client despite popup_unconstrain. Parent geometry and actual configure
must still be measured; different flags/geometry would change the contract.
9. Predicted A[-218,132)×[105,275),B[-118,182)×[165,295) cross0 for the last
content origin(-318,25). These are predictions, not static popup measurements.
10. Actual xdg_popup.configure,xdg_surface.configure/ACK/map,applied owner/root/
child scene positions and capture masks must establish both real crossings.
Missing crossing is NOT EXERCISED, never clipping PASS.
11. Root selection uses owner,chain and bounded observation window; ambiguous
roots stop. No arbitrary last trace. Historical indirect origin evidence is
identified; future direct PI_POPUP state must correlate the current owner.
12. Private root wrapper is globally parented; B is under A.xdg_surface_tree.
SceneFX ancestor clip traversal covers render and hit. This is source and
historical evidence, not new static applied-child measurement.
13. Shared RGB comparators intersect output and inherited viewport, subtract
B's occlusion from A, use actual configured rectangles and lifecycle.
14. Standard transition remeasures owner/content/root and recomputes A/B from
fresh origin; it never reuses Mosaic origin. Historical standard B local
(278,25) at global(900,190) is replayed.
15. Actual wl_pointer.button callbacks and WAYLAND_DEBUG requests bind distinct
press serials to each grab; synthetic tests have explicit labels. Runtime
errors/unaccepted grabs cannot be inferred away by source inspection.
16. Shared terminal_exchange preserves obtained IPC code/streams before wait;
scientific completeness, handled exit, compositor0 and protocol/cleanup gates
separately determine transport qualification. IPC7+timeout remains failed.
17. Independent review does not accept readiness: R02 survives. R01/R03 are
accepted repairs; initial accepted geometry/source scope remains unchanged.
18. Fixture is NOT READY for a new run. Smallest next gate is offline receipt
semantic completeness, not another compositor reservation.
## Final scope and retained evidence
Phase A was committed/pushed to both remotes at899c007c37beac03a337ba58ead4326ea8db8878
with a clean gate worktree. Phase B remains local, unstaged, uncommitted and
unpublished: report,17 source-only fixture files and five synchronized docs.
LAB results include all requested geometry/model/register/replay/test/review/
readiness/summary JSON, exact clients/protocols/private placement patch, source
contract copies, offline command receipts and review reports. New source and
evidence manifests are sealed once after finalization, with separate seal
receipt; historical manifests and ledgers remain immutable.
New runs/pristine runs/Mosaic builds/SceneFX builds/captures/pointer actions/grabs/
camera operations/installations/runtime reservations: **all0**. Client C17 builds
only, never executed. Static binary and310 protected source/system paths remain
unchanged. No production/patch/PKGBUILD/AGENTS/UX/PACKAGING/system/desktop IPC/
QuickShell/dotfiles/Codex/STEP20D operation. No experimental process/socket was
created by phase B. STEP20A DONE,STEP20B EXPERIMENTAL,STEP20C NEXT,STEP20D–G
PLANNED; production multi-output NOT YET SUPPORTED.
## Historical offline evidence freeze — 2026-10-13
This report and source fixture are preserved for publication by ticket
`SWAYFX_MOSAIC_STEP20C_NESTED_OFFLINE_FREEZE_AND_RECEIPT_INTEGRITY_V1`,
phase A. Statements about a local/unpublished phase above describe the prior
campaign, not the publication state of this historical freeze. No historical
receipt, review, manifest or fixture source was rewritten.
All 67 source and 88 evidence entries were verified individually against the
sealed manifests in `/home/fy59/swayfx-mosaic-static-nested-geometry-replay-a56csvoo/`.
Their SHA-256 values are respectively
`e1230ba1292f12d913b762f0678e638a2effb513b74eb44dd232c12aa4acea1d` and
`22b9ac035da95ba914c28d72d8aa6f019c16c2854095d81ceb62c0bd10da8dbe`.
The preserved writer SHA-256 is
`94ddab595dd9765d3edaa7158a6a98319f3be6b15a62842e4b10eeacfb530cfa`.
R01/R03 remain RESOLVED; R02 remains NOT_RESOLVED / CORRECTION_REQUIRED.
The three in-memory counterexamples in `results/parent-R02-reproduction.json`
are evidence of a validator defect, never compositor operation.
`SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE=INCONCLUSIVE`.
Architecture UNDECIDED. The 195 passing historical tests and 65 passing
independent targeted tests do not detect these semantic omissions. New static
popup runtime, serials, pixels, clicks, dismissal, standard return, atomic
generation and complete GPU-reference qualification remain NOT TESTED.
This freeze runs only static checks: no builds, graphical execution, runtime
budget or reservation. A separate local phase may repair R02; it cannot
retroactively change this historical verdict.

View file

@ -0,0 +1,169 @@
# Static nested geometry replay — EXPERIMENTAL offline fixture
This fixture corrects the frozen `../step20c-static-nested-grab/` experiment.
It does not implement production STEP20C and does not qualify the new static
popup scenario. Architecture remains UNDECIDED; new runtime is NOT TESTED.
The protocol was written before implementation in
[`STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md`](../../../docs/design/STEP20C_STATIC_NESTED_GEOMETRY_REPLAY_GATE.md).
The current ticket authorizes **offline reads, Python tests, protocol generation
and client-only C17 compilation**. It authorizes no compositor/client execution,
new capture, pointer, grab, camera, runtime/socket creation or execution ledger.
No runtime command is permitted by this README. Historical LABs, fixtures,
manifests and ledgers are read-only. Generated output belongs outside Git.
## Model and corrected paths
`model.py` uses immutable, half-open, tagged rectangles and owner/workspace/
observation-window provenance. NativeSHM, XDGConfigure, AppliedContent,
SceneGlobal, PopupLocal, GlobalViewport and OutputPNG are distinct. `content`
accounts explicitly for borders, titlebar and view offsets; `to_png` applies the
measured output origin after visible intersection. Scaling/transform without
measurement, pending state and mismatched provenance fail closed.
`observations.py` keeps native buffer create/attach/initial ACK/map separate
from subsequent configured destination/ACK. The historical client maps its
420×320 native SHM after configure0×0/ACK20, then receives636×573/ACK21 without
a replacement buffer. Applied content(-318,25,636,573), captured bbox
(482,25,800,598) and182214 blue pixels are separately corroborated. PNG does not
prove the identity of the native committed buffer/frame or atomic transaction.
`pixels.py` validates exact RGB masks using the same conversions for replay and
future runner. It accounts for output origin, inherited clip and B occluding A.
The opening point must also fit actual native input bounds: SceneFX destination
size alone does not enlarge the wlroots surface input region.
`run.py` is prepared for a separately authorized future ticket. E1 and E2 have
separate processes/owner identities and real left-button serials. Actual
configure/ACK/map, not the positioner request, drives A/B and pointer geometry;
missing crossing reports NOT EXERCISED. A bounded root/owner window must identify
one consistent root tree. Standard return remeasures owner/content origin and
root/tiled clip state with A/B still mapped, then measures B, explicitly closes
B, measures surviving A and finally compares the exact H2 reference. Dismissal
is separate from an invisible popup receiving a button. Cleanup records actual
IPC stdout/stderr/exit, handled compositor exit, process codes, reaping and
rescue. Missing scientific measurements cannot become success after clean exit.
`authorization.py` refuses before locks/debits/processes/runtime creation unless
a distinct explicit future authorization, completed accepted independent review,
ready marker and fresh registered LAB are present. The current offline LAB and
historical failed LAB are forbidden. This ticket does not initialize a runtime
budget. `ledger.py` creates ledgers only in test-owned temporary directories;
future registration is outside this ticket. Debits lock, validate and fsync
before returning; exhaustion, concurrency, corruption and failed compound
reservations are exercised, without refunds or resets. Future maxima remain
1 run,2 chains,4 grabs,2 camera operations (one per chain),1 transition,9 clicks,
16 PNG,24 positions,150 seconds.
## Exact offline commands
From the repository root, using the newly registered offline LAB (which must
already have `raw/` and `results/`):
```sh
LAB=/home/fy59/swayfx-mosaic-static-nested-geometry-replay-a56csvoo
FIXTURE=tooling/probes/step20c-static-nested-geometry-replay
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/prepare_clients.py" "$LAB"
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/replay.py" "$LAB"
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/tests_offline.py" "$LAB"
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/assertions.py" "$LAB"
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/assertions.py" "$LAB" --check
PYTHONDONTWRITEBYTECODE=1 python "$FIXTURE/write_results.py" "$LAB"
git diff --check
```
Preparation copies versioned nested/pointer/reference plus its included saved
client source, applies the byte-identical placement patch in private storage,
regenerates protocols and compares exact retained files. It compiles three
utilities with `-std=c17 -Wall -Wextra -Werror -Wno-unused-parameter`, without
executing them. No Mosaic/SceneFX build, package staging or installation occurs.
Future runtime requires only versioned sources and freshly discovered identities;
it does not read the old temporary historical LABs. Offline replay currently
reads the frozen failed LAB and old nested LAB explicitly; absent artifacts are
NOT AVAILABLE / NOT REPLAYED, never manufactured.
## Coverage and review
`assertions.py` enumerates every historical assertion (145), Defect/exit raises,
condition, resource/validation call, coordinate operation and latest/index
selection, plus the proposed runner/model. Source hashes and AST keys make
missing, duplicate, unclassified, stale and fabricated test receipts fail closed.
Per-entry positive/negative IDs refer to executed line or exact failed named
contract receipts. A reached line does not prove every conjunct. Retired history
has an explicit rationale; runtime-only observations remain NOT TESTED. The
register-format tests qualify only the checker itself, never scientific facts.
Core pure model/conversion/provenance/ledger/authorization/mask guards need real
positive and negative receipts. All remaining necessary unproved guards prevent
readiness. Inventory/classification completion is distinct from branch coverage.
`write_results.py` emits explicit readiness and requested JSON aliases. It never
signs the independent review marker. The independent configured reviewer must
review the final source delta, E1/E2/standard/cleanup, register and evidence and
write `independent-review.md/json` in the LAB. Before that review, the fixture is
**INCONCLUSIVE / prepared for independent review**, never READY. Manifests are
sealed only after parent review and final correction, outside this fixture.
## Bounded independent-review repairs R01–R03
The initial independent report remains immutable and CORRECTION_REQUIRED.
These repairs belong only to this new offline fixture and its external LAB.
They provide no new runtime result and no architectural decision.
R01: `correlate_historical` validates every identifiable local callback against
actual configured A/B and fresh standard origins through the shared
`pointer_local` predicate. The versioned injector starts at1000; motion and
button wire times bind each click to its global action. Wire callback numeric
values and surface identities must agree with client callbacks. Automatic
map retargets use the previous global point when the next motion precedes the
next button; surviving A after B close retains its observed local point.
Early seat callbacks before the first identifiable injected enter are retained
as NOT AVAILABLE / NOT REPLAYED with their scope. Software layout motion keeps
its actual wire time and last injected point; it acquires no fabricated
injection timestamp. All buttons are retained, paired and checked; the final
forbidden action is separated from earlier legitimate visible buttons and its
actual observed events feed dismissal. Corrupted coordinates, recipients,
extra invisible buttons and button order fail closed.
R02: `aggregate` is the single gate implementation used by writer and tests.
SHM, XDG/configured geometry, source contracts/pins, client provenance/C17,
all nine historical cases, register/coverage/core and test receipts are
mandatory and checked for freshness and structural presence. The bounded
review demonstrates that effective semantic completeness is still insufficient;
null geometry and bare PASS/empty popup records can evade these checks. An independent ACCEPTED review must bind the exact
`source_delta` and `evidence_sha256` published in runner-readiness; stale
acceptance blocks readiness. Marker values are exact PASS or INCONCLUSIVE;
`marker_scope` describes their limited offline meaning separately. Synthetic
acceptance used in tests exists in memory only. No author signs a review.
R03: the runner calls shared `terminal_exchange`, with injected executor/wait
functions in offline mocks. It stores the obtained IPC code and stdout/stderr
before fallible compositor wait, then records compositor exit/error separately.
IPC7 followed by wait timeout preserves7 and both streams, and stays a scientific
failure. Invocation failure keeps an explicit null IPC code. Completed measures
plus a clean handled compositor exit may retain IPC1 as a transport incident;
incomplete measures cannot become scientific success.
New aggregation negative receipts record the specific false gate and caller
line. They qualify offline rejection decisions, not graphical observations or
all conjuncts. The exhaustive current AST and all145 frozen historical asserts
remain inventoried. Re-run the offline sequence after source changes before
handing the final unsealed fixture to the parent for bounded review.
## Final offline disposition — INCONCLUSIVE / NOT READY
The independent tester ran195 tests with0 failures and all9 historical cases.
The bounded independent reviewer ran65 targeted tests PASS and resolved R01/R03,
but demonstrated R02 remains blocking for readiness: bare PASS input correlation,
null rendered values, or nine empty root records each produce erroneous synthetic
READY with the actual aggregate. The parent independently reproduced all three.
See the linked geometry-gate report for the retained findings, tested scope and
final assessed gate matrix. LAB/bounded-review.md and results/bounded-review.json
record CORRECTION_REQUIRED. Initial Astra report remains unchanged.
No independent acceptance exists. Actual readiness remains INCONCLUSIVE.
The four raw technical PASS labels do not prove effective receipt completeness.
The fixture is prepared but NOT READY; run.py must remain unexecuted. The next
step is a separately scoped offline correction of aggregate's semantic-content
guards and their negative regressions. No new runtime/budget is authorized.

View file

@ -0,0 +1,168 @@
#!/usr/bin/env python3
"""Exhaustive AST inventory, explicit history/proposal classification and receipts.
A reached line is not proof of every conjunct. Runtime-only entries are labelled
NOT TESTED, and no synthetic 'register valid' test is credited to their fact.
"""
import argparse
import ast
import hashlib
import json
from pathlib import Path
from model import require
from support import save,sha
HERE=Path(__file__).resolve().parent
REPO=HERE.parents[2]
HISTORY=HERE.parent/'step20c-static-nested-grab'
HISTORICAL_FILES=('run.py','predicates.py','ipc_predicates.py','geometry_audit.py')
RESOURCE_NAMES={'reserve','spawn','wait','ipc','cmd','capture','inject','click','find','snapshot','delivery','correlate_pointer','close_client','owner_state','open_chain','stop_owned','watchdog','terminal','terminal_exchange','aggregate','correlate_historical','verify','save','command','initial','initial_for_offline_test','authorize','durable','flock','Popen','run','killpg','poll','is_socket','wait','unlink','rmtree','close','write','flush','fsync','count','read_text','write_text'}
def inventory(path):
text=path.read_text();tree=ast.parse(text);parents={child:parent for parent in ast.walk(tree) for child in ast.iter_child_nodes(parent)}
records=[]
for node in ast.walk(tree):
kind=None
if isinstance(node,ast.Assert):kind='assert'
elif isinstance(node,ast.Raise):kind='raise/exit failure'
elif isinstance(node,(ast.If,ast.While)):kind='branch condition'
elif isinstance(node,ast.Try):kind='exception/closure path'
elif isinstance(node,ast.Compare):kind='comparison/identity condition'
elif isinstance(node,ast.Subscript) and isinstance(node.slice,ast.UnaryOp) and isinstance(node.slice.op,ast.USub):kind='latest/index selection'
elif isinstance(node,ast.BinOp) and isinstance(node.op,(ast.Add,ast.Sub,ast.Mult,ast.Div,ast.FloorDiv)):kind='coordinate arithmetic'
elif isinstance(node,ast.Call):
name=node.func.id if isinstance(node.func,ast.Name) else node.func.attr if isinstance(node.func,ast.Attribute) else ''
if name in {'require','need'}:kind='checked invariant'
elif name in RESOURCE_NAMES or name.startswith(('validate_','measure_','scene_')) or name in {'content','popup','same','intersect','to_png','from_png','verify_paint','pointer_local','fresh_chain','fresh_standard','constraints','local_clip_to_global','applied_model','output_model','viewport_model','verify_owner_occlusion','geometry','protocol','mapped','pair','dismissal','root_clip','popup_pixels','paint','point','equal','reference','configured','color_geometry'}:kind='validation/conversion/resource call'
if kind:
parent=node;function='<module>'
while parent in parents:
parent=parents[parent]
if isinstance(parent,(ast.FunctionDef,ast.AsyncFunctionDef)):
function=parent.name;break
expression=ast.get_source_segment(text,node) or ast.unparse(node)
# Expressions in branch/try containers can contain whole suites.
if isinstance(node,(ast.If,ast.While)):expression=ast.get_source_segment(text,node.test) or ast.unparse(node.test)
if isinstance(node,ast.Try):expression='try / '+','.join(ast.unparse(h.type) if h.type else 'bare' for h in node.handlers)+' / finally='+str(bool(node.finalbody))
canonical=ast.dump(node.test if isinstance(node,(ast.Assert,ast.If,ast.While)) else node,include_attributes=False)
key=f'{path.relative_to(REPO)}:{node.lineno}:{node.col_offset}:{node.end_lineno}:{node.end_col_offset}:{kind}'
contract=None
if isinstance(node,ast.Call) and kind=='checked invariant' and len(node.args)>1 and isinstance(node.args[1],ast.Constant):contract=node.args[1].value
records.append(dict(id=key,source=str(path.relative_to(REPO)),line=node.lineno,column=node.col_offset,function=function,kind=kind,invariant=expression,canonical_hash=hashlib.sha256(canonical.encode()).hexdigest(),contract=contract))
return sorted(records,key=lambda r:(r['line'],r['column'],r['kind']))
def classify(r):
text=r['invariant'];fn=r['function'];src=r['source']
if fn=='correlate_historical' or any(w in (fn+' '+text).lower() for w in ('serial','protocol','ack','xdg','mapped','configure','parent','grab','dismiss','button','pair')):
domain='XDG lifecycle/input';support=['wlroots types/xdg_shell/wlr_xdg_popup.c retained source-audit.json:configure/unconstrain','xdg-shell.xml ACK/map/parent/grab protocol','actual WAYLAND_DEBUG/client.log']
elif any(w in (fn+' '+text).lower() for w in ('terminal','exit','cleanup','rescue','reap','kill','poll','process','socket','watchdog','wait','expire','time','code')):
domain='terminal/owned resources';support=['actual stdout/stderr/process exit; no causal packet claim','sway/commands/exit.c and sway/main.c shutdown']
elif any(w in (fn+' '+text).lower() for w in ('owner','workspace','focus','camera','scroll','reference','output','scene','clip','geometry','content','paint','png','buffer','height','width','origin','rect','point','pixel','bounds')):
domain='typed geometry/assignment';support=['source-audit.json: output.c destination, transaction.c applied arrangement, ipc-json.c window_rect','SceneFX wlr_scene.c inherited clipping/render/hit; wlroots scene surface native input','actual IPC/applied traces and independent RGB']
elif any(w in (fn+' '+text).lower() for w in ('ledger','budget','reserve','limit','debit','auth','gate','freeze','hash','manifest','sha','identity','inventory')):
domain='authorization/provenance/budget';support=['offline gate explicit authorization and durable maxima','source hashes / exact files / typed identity provenance']
else:
domain='operational pure guard';support=['Python/C fixture operational contract; synthetic error branch permissible','offline gate scope']
history='step20c-static-nested-grab/' in src
decision='retain'
rationale='Retain checked fact/operation; measurements remain independently required.'
# Frozen invalid assumptions and obsolete one-ticket authorization are replaced.
if history and ('topbox[3]-topbox[1]==320' in text or 'origin[1]==after' in text):
decision='correct';rationale='Historical failure reproduced: native SHM height differs from rendered destination; titlebar-dependent IPC y excludes actual content offset. Replaced by model.content/verify_paint.'
elif history and ('rows[-1]' in text and fn=='root_clip'):
decision='replace';rationale='Latest arbitrary root is ambiguous. Proposed bounded time/owner/unique tree correlation fails closed.'
elif history and ('configured_A' in text and '==[100,80' in text):
decision='replace';rationale='Requested placement is source-backed prediction; actual configure/ACK/map is measured and crossing can be NOT EXERCISED.'
elif history and ('OWNER' in text or 'STATIC_NESTED_GRAB_FIXTURE_PREFLIGHT' in text or fn=='<module>' and 'reserve(lab' in text):
decision='replace';rationale='Historical authorization/ledger cannot authorize new run; future gate precedes all creation/debit.'
elif history and fn=='validate_preflight' and ('commit[' in text or 'SavedBufferProbe' in text):
decision='remove';rationale='Saved-buffer probe validator is not the native420x320 nested client contract. Applied/native/configure are correlated independently by shared model.'
elif history and src.endswith('geometry_audit.py'):
decision='retain historical only';rationale='Frozen diagnostic facts retained; new independent replay reads actual inputs without executing the failed runner.'
stage={'open_chain':'E1/E2 mapped Mosaic','owner_state':'owner/camera observation','correlate_pointer':'visible pointer correlation','close_client':'ordered client close','root_clip':'bounded root clip','terminal':'terminal cleanup','protocol':'XDG valid-grab chain','popup_pixels':'rendered popup mask','geometry':'actual configured popup geometry','replay_native':'historical E1','replay_nested':'historical popup/standard/dismissal','authorize':'pre-runtime refusal','reserve':'durable reservation','content':'native/configure/applied/rendered conversion'}.get(fn,fn)
# CONTRACT: aggregate and terminal_exchange receipts prove offline decisions
# only; their successful mocks never become new runtime observations.
if fn in {'aggregate','need'}:
domain='authorization/provenance/budget'
support=['mandatory offline evidence freshness/completeness and independent bound acceptance']
r.update(history='frozen historical' if history else 'corrected proposed offline fixture',stage=stage,domain=domain,source_protocol_evidence_support=support,replay_possible=not (src.endswith('run.py') or fn in {'spawn','watchdog'}),decision=decision,rationale=rationale)
return r
def build(lab):
paths=[HISTORY/n for n in HISTORICAL_FILES]+[p for p in sorted(HERE.glob('*.py')) if p.name!='tests_offline.py']
allrecords=[classify(r) for p in paths for r in inventory(p)]
tests=json.loads((lab/'results/test-receipts.json').read_text())['tests']
receipts={r['id']:r for r in tests if r['status']=='PASS'}
by_hash={}
for r in allrecords:
if r['history'].startswith('corrected'):by_hash.setdefault(r['canonical_hash'],[]).append(r)
for r in allrecords:
corresponding=[r]+(by_hash.get(r['canonical_hash'],[]) if r['history']=='frozen historical' else [])
positive=[];negative=[]
for tid,test in receipts.items():
lines=set(test.get('executed_lines',[]))
executed=any(str(REPO/c['source'])+':'+str(c['line']) in lines for c in corresponding)
contracts=test.get('contracts',[])
failed_contract=r.get('contract') and any(c['contract']==r['contract'] and not c['pass'] for c in contracts)
if executed and test['mode']=='positive' and not (r['domain']=='authorization/provenance/budget' and r['function'] in {'aggregate','need'} and 'inventory_' in tid):positive.append(tid)
if failed_contract:negative.append(tid)
elif executed and any(str(REPO/c['source'])+':'+str(c['line']) in test.get('failed_lines',[]) for c in corresponding):negative.append(tid)
# Exact known historical semantic defects have explicit replacement tests.
if r['decision']=='correct':
suffix='negative_native_height' if '320' in r['invariant'] else 'negative_scene_window_y'
negative += [tid for tid in receipts if tid.endswith(suffix)]
positive += [tid for tid in receipts if tid.endswith('real_native_replay')]
r['positive_executed_test_ids']=sorted(set(positive));r['negative_executed_test_ids']=sorted(set(negative))
r['coverage_meaning']='executed line / exact require-contract failure or recorded false aggregation gate; conjunct completeness not implied'
r['future_runtime_required']=r['source'].endswith('/run.py') or r['domain'] in {'XDG lifecycle/input','terminal/owned resources'}
r['test_status']='RETIRED historical contract with explicit rationale' if r['decision']=='remove' else 'PASS executed positive/negative branch' if positive and negative else 'PARTIAL positive replay' if positive else 'NOT TESTED runtime dependency' if r['future_runtime_required'] else 'NOT TESTED pure branch'
if not positive or not negative:
r['untested_reason']='Live applied/input/cleanup fact requires future authorized execution; historical or synthetic receipt only proves listed observations.' if r['future_runtime_required'] else 'Branch inventoried; no claim of executed negative/positive coverage. Independent review must decide whether this pure branch is necessary for readiness.'
files={str(p.relative_to(REPO)):sha(p) for p in paths}
scientific_core={'model.py','ledger.py','authorization.py','observations.py','pixels.py'}
unsupported=[r['id'] for r in allrecords if Path(r['source']).name in scientific_core and r['kind']=='checked invariant' and not (r['positive_executed_test_ids'] and r['negative_executed_test_ids'])]
save(lab,'offline-core-coverage',dict(status='PASS' if not unsupported else 'FAIL NOT PROVEN',unproved=unsupported))
save(lab,'assertion-register',dict(status='CLASSIFIED; execution status is per-entry',source_inventory=files,artifact_inventory={str(p):sha(p) for p in HERE.iterdir() if p.suffix in ('.patch','.json')},records=allrecords,counts={kind:sum(r['kind']==kind for r in allrecords) for kind in sorted({r['kind'] for r in allrecords})},historical_asserts=sum(r['kind']=='assert' and r['history']=='frozen historical' for r in allrecords)))
return check(lab)
def check(lab):
register=json.loads((lab/'results/assertion-register.json').read_text());records=register['records']
actual={r['id']:r for rel in register['source_inventory'] for r in inventory(REPO/rel)}
require(len(records)==len({r['id'] for r in records}) and set(actual)=={r['id'] for r in records},'register-exhaustive-unique')
require(all(sha(REPO/rel)==digest for rel,digest in register['source_inventory'].items()) and all(sha(p)==digest for p,digest in register.get('artifact_inventory',{}).items()),'register-source-freshness')
tests=json.loads((lab/'results/test-receipts.json').read_text())['tests'];passed={r['id'] for r in tests if r['status']=='PASS'}
require(all(r['stage'] and r['domain'] and r['source_protocol_evidence_support'] and r['decision'] and r['rationale'] for r in records),'register-classified')
require(all(r['canonical_hash']==actual[r['id']]['canonical_hash'] for r in records),'register-ast-freshness')
require(all(set(r['positive_executed_test_ids']+r['negative_executed_test_ids'])<=passed for r in records),'register-executed-receipts')
byhash={}
for r in records:
if r['history'].startswith('corrected'):byhash.setdefault(r['canonical_hash'],[]).append(r)
proof={r['id']:r for r in tests if r['status']=='PASS'}
def claimed(r,tid,negative):
t=proof[tid];peers=[r]+(byhash.get(r['canonical_hash'],[]) if r['history']=='frozen historical' else [])
lines=t.get('failed_lines' if negative else 'executed_lines',[])
if any(str(REPO/c['source'])+':'+str(c['line']) in lines for c in peers):return True
if negative and r.get('contract') and any(c['contract']==r['contract'] and not c['pass'] for c in t.get('contracts',[])):return True
if r['decision']=='correct':
if not negative:return tid.endswith('real_native_replay')
name='negative_native_height' if '320' in r['invariant'] else 'negative_scene_window_y'
return tid.endswith(name) and any(c['contract']=='paint-origin-intersection' and not c['pass'] for c in t.get('contracts',[]))
return False
require(all(claimed(r,tid,False) for r in records for tid in r['positive_executed_test_ids']) and
all(claimed(r,tid,True) for r in records for tid in r['negative_executed_test_ids']), 'register-predicate-receipt-correlation')
receipt_inventory=json.loads((lab/'results/test-receipts.json').read_text()).get('source_inventory',{})
require(all(sha(p)==digest for p,digest in receipt_inventory.items()),'test-receipt-source-freshness')
core=json.loads((lab/'results/offline-core-coverage.json').read_text()) if (lab/'results/offline-core-coverage.json').exists() else None
if core is not None:require(core.get('status')=='PASS','offline-core-untested-rejected')
require(sum(r['kind']=='assert' and r['history']=='frozen historical' for r in records)==145,'historical-145-assertions')
unresolved=[r['id'] for r in records if r['test_status']=='NOT TESTED pure branch' and r['kind']=='checked invariant']
result=dict(status='PASS AST inventory/freshness/classification; PARTIAL executed branch coverage' if unresolved else 'PASS',entries=len(records),historical_asserts=145,positive_and_negative=sum(bool(r['positive_executed_test_ids'] and r['negative_executed_test_ids']) for r in records),positive_only=sum(bool(r['positive_executed_test_ids']) and not r['negative_executed_test_ids'] for r in records),unexecuted=sum(not r['positive_executed_test_ids'] and not r['negative_executed_test_ids'] for r in records),unresolved_pure_invariants=unresolved,runtime_facts='NOT TESTED; no generic register test credited')
save(lab,'assertion-coverage',result);return result
if __name__=='__main__':
parser=argparse.ArgumentParser();parser.add_argument('lab',type=Path);parser.add_argument('--check',action='store_true');args=parser.parse_args()
print(json.dumps(check(args.lab) if args.check else build(args.lab),indent=2))

View file

@ -0,0 +1,26 @@
"""Pure refusal gate. No files/locks/processes are created by validation."""
import json
from pathlib import Path
from model import require
MARKER = 'SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE=READY_FOR_NEW_RUNTIME'
THIS_TICKET = 'static-nested-geometry-offline-replay'
def authorize(lab, authorization):
require(authorization is not None, 'explicit-future-authorization-required')
auth = json.loads(Path(authorization).read_text())
require(auth.get('scope') == 'one-new-static-nested-headless-run' and
auth.get('explicit_user_authorization') is True and
auth.get('ticket') and auth['ticket'] != THIS_TICKET, 'distinct-future-ticket-required')
lab = Path(lab).resolve()
require(auth.get('registered_lab') == str(lab), 'registered-fresh-lab-required')
require('static-nested-grab-m0a5e2qh' not in str(lab) and
'static-nested-geometry-replay-a56csvoo' not in str(lab), 'historical-or-offline-lab-forbidden')
gate = json.loads((lab/'results/offline-gate.json').read_text())
review = json.loads((lab/'results/independent-review.json').read_text())
require(gate.get('marker') == MARKER and review.get('status') == 'ACCEPTED' and
review.get('independent') is True, 'completed-offline-review-required')
require(not (lab/'run').exists(), 'fresh-run-required')
require(all(auth.get(k) for k in ('owner_registry', 'binary', 'binary_sha256', 'wlroots_sha256')), 'future-input-provenance')
return auth

View file

@ -0,0 +1,13 @@
{
"status": "EXPERIMENTAL exact retained historical client/protocol byte contract",
"source_receipt": "client-provenance.json in offline LAB; scanner must reproduce exact hashes",
"adapted_nested_sha256": "6eafb8ad63b0b06b8297e7e72711056a6d42bdf33ccf795793eeda77f98221c7",
"placement_sha256": "e0e87fb0cb3d6e7dafb1cd59ccb50f323f2934e65247526199da1695487d3e4a",
"protocols": {
"xdg-shell-client.h": "a09726137ea9fe1a23d58c95f1d33ab77a3fc692c63726bc82fbc91ab8e5c6fc",
"xdg-shell-protocol.c": "9e12fcd5676d8c6b6cfd233c2eba563163c0ea7e586cb6e27f202a328323c7f0",
"virtual-pointer-client.h": "0dcb6107cf948a007dcef0a6b2192e4f7b9166c0f57b499ca49b7aaf48adc56c",
"virtual-pointer-protocol.c": "a72e9b38dd5ed0c49fae22aa2f01883aea76075ad33f6399d9b2033df4330675"
},
"native_nested_sha256": "2e40c98af72a0df8b316810589a0be8f4425a763db1de448b49a7813956b6f7d"
}

View file

@ -0,0 +1,111 @@
"""Pure validators for replay and live observations, never desktop IPC.
WHY: stored border thickness and container IPC geometry are not rendered pixels.
CONTRACT: callers supply measured identities; validate ancestors and applied scene.
INVARIANT: no width-zero predicate, hard-coded runtime IDs, or native buffer y.
"""
import re
OUTPUTS = {'HEADLESS-1': (-800, 0, 800, 600, 1.0, 'normal'),
'HEADLESS-2': (0, 0, 800, 600, 1.0, 'normal')}
ZERO = dict(x=0, y=0, width=0, height=0)
FULL = dict(x=0, y=0, width=800, height=600)
def nodes(node):
yield node
for child in node.get('nodes', []) + node.get('floating_nodes', []):
yield from nodes(child)
def workspace(tree, name):
rows = [n for n in nodes(tree) if n.get('type') == 'workspace' and n.get('name') == name]
assert len(rows) == 1, 'workspace identity'
return rows[0]
def ancestry(tree, con_id, path=()):
if tree.get('id') == con_id:
return path + (tree,)
for child in tree.get('nodes', []) + tree.get('floating_nodes', []):
found = ancestry(child, con_id, path + (tree,))
if found:
return found
return ()
def validate_outputs(outputs):
actual = {o['name']: (*[o['rect'][k] for k in ('x', 'y', 'width', 'height')],
o['scale'], o['transform']) for o in outputs if o['active']}
assert actual == OUTPUTS, ('output geometry', actual)
assert len([o for o in outputs if o['active']]) == 2, 'duplicate output'
return actual
def validate_reference(snapshot, con_id, pid, workspace_name='2', output_name='HEADLESS-2'):
"""B_NONE may retain width 2; require actual empty decoration/full content.
IPC visibility means view_is_visible, not proof of SHM coverage. RGB is
independently required by the runner. Width is returned only as metadata.
"""
validate_outputs(snapshot['outputs'])
path = ancestry(snapshot['tree'], con_id)
assert path, 'reference surface absent'
ref = path[-1]
ws = next((n for n in path if n.get('type') == 'workspace'), None)
out = next((n for n in path if n.get('type') == 'output'), None)
assert ref.get('type') == 'con' and ref.get('shell') == 'xdg_shell', 'reference view absent'
assert ref.get('app_id') == 'org.mosaic.StaticReference', 'reference App ID'
assert ref.get('pid') == pid and pid > 0 and ref['id'] == con_id, 'reference PID/ID'
assert ws and ws['name'] == workspace_name and ws.get('output') == output_name, 'reference workspace'
assert out and out['name'] == output_name and out['rect'] == FULL, 'reference output'
assert ref.get('visible') is True, 'reference visibility'
assert ref.get('border') == 'none', 'reference border mode'
assert ref.get('rect') == FULL and ref.get('window_rect') == FULL, 'reference full content'
assert ref.get('deco_rect') == ZERO, 'effective reference decoration'
return {'status': 'PASS', 'con_id': con_id, 'pid': pid, 'workspace': ws['id'],
'output': output_name, 'stored_border_width': ref.get('current_border_width'),
'reference': ref}
def scene_from_log(text, output):
rows = [s for s in text.splitlines() if 'PI_SCENE output=' + output + ' ' in s
and 'workspace=none' not in s]
assert rows, 'applied scene trace absent'
line = rows[-1]
m = re.search(r'workspace=(\d+) layout=(\d+) scroll=(-?[\d.]+) tile_scene=(-?\d+),(-?\d+) clip_valid=(\d+) clip=(-?\d+),(-?\d+),(\d+),(\d+)', line)
assert m, 'scene trace format'
v = list(map(float, m.groups()))
origin = OUTPUTS[output][:2]
return {'workspace': int(v[0]), 'layout_enum': int(v[1]), 'scroll': v[2],
'tile_local': v[3:5], 'clip_valid': bool(v[5]), 'clip_local': v[6:10],
'global_clip': [origin[0] + v[3] + v[6], origin[1] + v[4] + v[7], v[8], v[9]],
'raw': line}
def measure_owner(text, owner):
rows = [x for x in text.splitlines() if 'PI_OWNER output=HEADLESS-1 ' in x
and f' id={owner["id"]} ' in x]
assert rows, 'applied owner trace absent'
line = rows[-1]
m = re.search(r'scene_valid=1 scene=(-?\d+),(-?\d+) applied_size=(\d+),(\d+)', line)
assert m, 'owner trace format'
x, y, w, h = map(int, m.groups())
win = owner['window_rect']
return {'id': owner['id'], 'scene': [x, y, w, h], 'window_rect': win,
'horizontal_content': [x + win['x'], win['width']], 'raw': line, 'IPC': owner}
def client_commit(text):
rows = [s for s in text.splitlines() if s.startswith('COMMIT ')]
assert rows, 'no real client commit'
m = re.fullmatch(r'COMMIT ns=(\d+) serial=(\d+) size=(\d+)x(\d+) color=([0-9a-f]{8})', rows[-1])
assert m, 'client commit format'
ns, serial, w, h = map(int, m.groups()[:4])
assert ns > 0 and 0 < serial <= 0xffffffff and 0 < w <= 4096 and 0 < h <= 4096
return {'ns': ns, 'serial': serial, 'width': w, 'height': h, 'color': m[5], 'raw': rows[-1]}
def validate_camera(before_scroll, after_scroll, delta, scene):
assert type(delta) is int and -2147483647 <= delta <= 2147483647
assert after_scroll == before_scroll + delta and scene['scroll'] == after_scroll, 'camera correction applied'

View file

@ -0,0 +1,65 @@
"""Durable debits. Offline tests initialize temporary ledgers only.
The offline LAB never has a runtime ledger. Future registration is a separate
explicitly authorized ticket; failed reservations/actions are never refunded.
"""
import fcntl
import json
import os
from pathlib import Path
import tempfile
import time
from model import require
LIMITS = dict(run=1, chain=2, grab=4, click=9, capture=16, camera=2, transition=1, move=24)
def durable(path, state):
fd, tmp = tempfile.mkstemp(prefix='.debit-', dir=path.parent)
try:
with os.fdopen(fd, 'w') as out:
json.dump(state, out); out.flush(); os.fsync(out.fileno())
os.replace(tmp, path)
fd = os.open(path.parent, os.O_RDONLY | os.O_DIRECTORY)
try:
os.fsync(fd)
finally:
os.close(fd)
finally:
if os.path.exists(tmp):
os.unlink(tmp)
def initial_for_offline_test(path):
"""No production initialization API: the caller proves isolated test storage."""
path = Path(path)
require(path.parent.name.startswith('geometry-ledger-test-'), 'test-ledger-only')
with path.open('x') as out:
json.dump(dict(limits=LIMITS, used=dict.fromkeys(LIMITS, 0), events=[]), out)
out.flush(); os.fsync(out.fileno())
def valid(state):
require(state.get('limits') == LIMITS and set(state.get('used', {})) == set(LIMITS), 'ledger-schema')
require(all(type(state['used'][k]) is int and 0 <= state['used'][k] <= LIMITS[k] for k in LIMITS), 'ledger-counts')
events = state.get('events')
require(isinstance(events, list) and len(events) == sum(state['used'].values()), 'ledger-events')
require(all(isinstance(e, dict) and e.get('seq') == i and e.get('kind') in LIMITS and
type(e.get('ns')) is int and e['ns'] > 0 for i, e in enumerate(events)), 'ledger-sequences')
require(all(sum(e['kind'] == k for e in events) == state['used'][k] for k in LIMITS), 'ledger-accounting')
return state
def reserve(path, *kinds):
path = Path(path)
require(path.is_file() and not path.is_symlink(), 'existing-ledger-required')
with path.with_suffix('.lock').open('a+') as lock:
fcntl.flock(lock, fcntl.LOCK_EX)
state = valid(json.loads(path.read_text()))
require(bool(kinds) and all(k in LIMITS for k in kinds), 'ledger-debit-kinds')
require(all(state['used'][k] + kinds.count(k) <= LIMITS[k] for k in kinds), 'ledger-exhausted')
for k in kinds:
state['used'][k] += 1
state['events'].append(dict(seq=len(state['events']), kind=k, ns=time.monotonic_ns()))
durable(path, state)
return state

View file

@ -0,0 +1,194 @@
"""EXPERIMENTAL typed half-open geometry. Pure: no processes or sockets.
Source contracts are recorded in the offline gate, not inferred from RGB.
Every conversion is explicit and keeps assignment/owner/generation provenance.
"""
from dataclasses import dataclass
from enum import Enum
class Invalid(ValueError):
pass
class Space(str, Enum):
NATIVE = 'NativeSHM'
CONFIGURE = 'XDGConfigure'
CONTENT = 'AppliedContent'
GLOBAL = 'SceneGlobal'
POPUP = 'PopupLocal'
VIEWPORT = 'GlobalViewport'
PNG = 'OutputPNG'
def require(value, contract):
if not value:
raise Invalid(contract)
@dataclass(frozen=True)
class Provenance:
owner: int
workspace: int
generation: str
evidence: str
state: str = 'applied'
@dataclass(frozen=True)
class Rect:
space: Space
x: int
y: int
width: int
height: int
provenance: Provenance
def __post_init__(self):
require(isinstance(self.space, Space), 'tag-required')
require(all(type(v) is int for v in (self.x, self.y, self.width, self.height)), 'integer-geometry')
require(self.width >= 0 and self.height >= 0, 'nonnegative-size')
require(bool(self.provenance.evidence), 'evidence-required')
@property
def end(self):
return (self.x + self.width, self.y + self.height)
def contains(self, xy):
return self.x <= xy[0] < self.end[0] and self.y <= xy[1] < self.end[1]
def values(self):
return [self.x, self.y, self.width, self.height]
@dataclass(frozen=True)
class Native:
rectangle: Rect
buffer_id: int
stride: int
format: int
commit_serial: int
@dataclass(frozen=True)
class Applied:
scene: Rect
window: Rect
configured: Rect
native: Native
border_left: int
border_top: int
titlebar: int
configure_ack: int
view_offset: tuple = (0, 0)
@dataclass(frozen=True)
class Output:
name: str
rectangle: Rect
scale: float
transform: str
def same(a, b):
require(a.owner == b.owner, 'owner-identity')
require(a.workspace == b.workspace, 'workspace-identity')
require(a.generation == b.generation, 'applied-generation')
require(a.state == b.state == 'applied', 'pending-not-applied')
def content(applied):
s, w, c, n = applied.scene, applied.window, applied.configured, applied.native
require(s.space is Space.GLOBAL and w.space is Space.CONTENT and c.space is Space.CONFIGURE,
'assignment-spaces')
require(n.rectangle.space is Space.NATIVE, 'native-space')
for r in (w, c, n.rectangle):
same(s.provenance, r.provenance)
require(n.buffer_id > 0 and n.stride == n.rectangle.width * 4 and n.format in (0, 1), 'native-buffer-identity')
require(0 < n.commit_serial <= 0xffffffff, 'commit-serial')
require(0 < applied.configure_ack <= 0xffffffff, 'assigned-configure-ack')
require((w.width, w.height) == (c.width, c.height), 'configure-assignment')
require(applied.border_left == w.x and applied.border_top == applied.titlebar + w.y,
'titlebar-content-offset')
require(w.width + 2 * applied.border_left == s.width and
w.height + applied.border_top + applied.border_left == s.height, 'assigned-destination')
return Rect(Space.GLOBAL, s.x + applied.border_left + applied.view_offset[0],
s.y + applied.border_top + applied.view_offset[1], w.width, w.height, s.provenance)
def intersect(rect, boundary):
require(rect.space is Space.GLOBAL and boundary.space in (Space.GLOBAL, Space.VIEWPORT), 'global-intersection')
same(rect.provenance, boundary.provenance)
x, y = max(rect.x, boundary.x), max(rect.y, boundary.y)
return Rect(Space.GLOBAL, x, y, max(0, min(rect.end[0], boundary.end[0]) - x),
max(0, min(rect.end[1], boundary.end[1]) - y), rect.provenance)
def to_png(rect, output):
require(rect.space is Space.GLOBAL and output.rectangle.space is Space.GLOBAL, 'global-to-png-spaces')
require(output.scale == 1.0, 'unmeasured-output-scale')
require(output.transform == 'normal', 'unmeasured-output-transform')
same(rect.provenance, output.rectangle.provenance)
visible = intersect(rect, output.rectangle)
return Rect(Space.PNG, min(max(visible.x - output.rectangle.x,0),output.rectangle.width), min(max(visible.y - output.rectangle.y,0),output.rectangle.height),
visible.width, visible.height, rect.provenance)
def from_png(rect, output):
require(rect.space is Space.PNG and output.rectangle.space is Space.GLOBAL, 'png-to-global-spaces')
require(output.scale == 1.0 and output.transform == 'normal', 'unmeasured-png-transform')
same(rect.provenance, output.rectangle.provenance)
require(0 <= rect.x <= rect.end[0] <= output.rectangle.width and
0 <= rect.y <= rect.end[1] <= output.rectangle.height, 'png-bounds')
return Rect(Space.GLOBAL, rect.x + output.rectangle.x, rect.y + output.rectangle.y,
rect.width, rect.height, rect.provenance)
def verify_paint(rect, output, bbox, count, clip=None):
expected = to_png(intersect(rect, clip) if clip is not None else rect, output)
actual = [] if bbox is None else list(bbox)
box=[expected.x, expected.y, *expected.end] if expected.width and expected.height else []
require(actual == box, 'paint-origin-intersection')
require(count == expected.width * expected.height, 'paint-area')
return expected
def popup(parent, configured, parent_xdg, expected_parent_xdg, ack, mapped):
require(parent.space is Space.GLOBAL and configured.space is Space.POPUP, 'popup-spaces')
same(parent.provenance, configured.provenance)
require(parent_xdg == expected_parent_xdg and expected_parent_xdg > 0, 'xdg-parent')
require(0 < ack <= 0xffffffff, 'popup-ack')
require(mapped is True, 'popup-map')
return Rect(Space.GLOBAL, parent.x + configured.x, parent.y + configured.y,
configured.width, configured.height, parent.provenance)
def crossing(rect, boundary_x):
require(rect.space is Space.GLOBAL, 'crossing-space')
return 'EXERCISED' if rect.x < boundary_x < rect.end[0] else 'NOT EXERCISED'
def local_clip_to_global(local, origin, provenance):
require(local.space is Space.CONTENT, 'clip-local-space')
same(local.provenance, provenance)
return Rect(Space.VIEWPORT, local.x + origin[0], local.y + origin[1],
local.width, local.height, provenance)
def pointer_local(xy, rect, actual):
require(rect.space is Space.GLOBAL and rect.contains(xy), 'pointer-global-bounds')
require(list(actual) == [xy[0] - rect.x, xy[1] - rect.y], 'pointer-local-correlation')
return list(actual)
def fresh_chain(old, new):
require(old['owner'] != new['owner'] and old['pid'] != new['pid'], 'fresh-E2-identity')
require(len(set(old['serials'] + new['serials'])) == 4 and
max(old['serials']) < min(new['serials']), 'fresh-E2-serials')
def fresh_standard(mosaic, standard):
require(mosaic.provenance.owner == standard.provenance.owner and
mosaic.provenance.workspace == standard.provenance.workspace, 'standard-owner')
require(mosaic.provenance.generation != standard.provenance.generation, 'fresh-standard-generation')
return standard
def constraints(flags, requested, configured):
require(type(flags) is int and 0 <= flags <= 63, 'positioner-flags')
require(flags != 0 or requested == configured, 'zero-flags-no-adjustment')
return {'flags': flags, 'request': requested, 'actual': configured, 'prediction_only': True}

View file

@ -0,0 +1,59 @@
"""Adapters from independently recorded protocol/IPC/applied trace observations.
No native-buffer/frame identity is attributed to a screenshot. Generation is
an observation-window label; atomic transaction-generation is NOT TESTED.
"""
import re
from model import *
def applied_model(measured, owner, text, generation):
require(measured['id'] == owner['id'] and measured['IPC'] == owner, 'measured-owner-identity')
workspace = measured.get('workspace')
require(workspace is not None, 'measured-workspace-required')
p = Provenance(owner['id'], workspace, generation, measured['raw'])
buffers = re.findall(r'create_buffer\(new id wl_buffer#(\d+), \d+, (\d+), (\d+), (\d+), (\d+)\)', text)
require(bool(buffers), 'native-shm-trace-required')
# Top's first buffer is recorded before TOPLEVEL MAP; never choose popup buffer.
first = re.search(r'create_buffer\(new id wl_buffer#(\d+), \d+, (\d+), (\d+), (\d+), (\d+)\)', text)
require(first.start() < text.index('TOPLEVEL MAP '), 'toplevel-buffer-before-map')
bid,w,h,stride,fmt = map(int, first.groups())
top_id=int(re.search(r'TOPLEVEL CREATE wl=(\d+)',text)[1])
require(re.search(rf'wl_surface#{top_id}\.attach\(wl_buffer#{bid}, 0, 0\)',text) is not None,'native-toplevel-attach')
cfgs = re.findall(r'TOPLEVEL ROLE_CONFIGURE w=(\d+) h=(\d+)', text)
configured = next((list(map(int,c)) for c in reversed(cfgs) if int(c[0]) > 0 and int(c[1]) > 0), None)
require(configured is not None, 'toplevel-configure-required')
assigned_ack = int(re.findall(r'TOPLEVEL XDG_CONFIGURE serial=(\d+) ack', text)[-1])
require(f'ack_configure({assigned_ack})' in text, 'assigned-ack-trace')
serial = int(re.search(r'TOPLEVEL XDG_CONFIGURE serial=(\d+) ack', text)[1])
natural=owner['geometry']
require(natural==dict(x=0,y=0,width=w,height=h),'native-natural-geometry')
win = owner['window_rect']
return Applied(Rect(Space.GLOBAL,*measured['scene'],p),
Rect(Space.CONTENT,*[win[k] for k in ('x','y','width','height')],p),
Rect(Space.CONFIGURE,0,0,*configured,p),
Native(Rect(Space.NATIVE,0,0,w,h,p),bid,stride,fmt,serial),
win['x'], owner['deco_rect']['height'] + win['y'], owner['deco_rect']['height'],assigned_ack)
def output_model(snapshot, name, provenance):
outputs = [o for o in snapshot['outputs'] if o['name'] == name and o['active']]
require(len(outputs) == 1, 'unique-active-output')
o = outputs[0]
return Output(name,Rect(Space.GLOBAL,*[o['rect'][k] for k in ('x','y','width','height')],provenance),o['scale'],o['transform'])
def viewport_model(scene, provenance):
require(scene['workspace'] == provenance.workspace, 'viewport-workspace')
require(scene['clip_valid'] is True, 'viewport-applied-valid')
return Rect(Space.VIEWPORT,*map(int,scene['global_clip']),provenance)
def verify_owner_occlusion(left,right,rect,g,mosaic):
from pixels import color_geometry
p=rect.provenance
occluders=tuple(Rect(Space.GLOBAL,*g[k],p) for k in ('A','B'))
for im,ox in ((left,-800),(right,0)):
out=Output(str(ox),Rect(Space.GLOBAL,ox,0,800,600,p),1.0,'normal')
clip=Rect(Space.VIEWPORT,-800,0,800,600,p) if mosaic else None
color_geometry(im,'TOPLEVEL',rect,out,clip,occluders)

View file

@ -0,0 +1,21 @@
"""Exact binary RGB masks with explicit output origin, clip and occlusion.
Screenshots prove color/visible geometry only, never native-buffer identity.
"""
from PIL import Image,ImageChops,ImageDraw
from model import *
COLORS=dict(TOPLEVEL=(35,68,204),POPUP_A=(224,192,32),POPUP_B=(32,208,160))
def color_geometry(im,target,rect,output,clip,occluders=()):
require(im.size==(output.rectangle.width,output.rectangle.height),'replay-output-size')
visible=intersect(rect,clip) if clip else rect
expected=Image.new('L',im.size,0);draw=ImageDraw.Draw(expected)
box=to_png(visible,output)
if box.width and box.height:draw.rectangle((box.x,box.y,box.end[0]-1,box.end[1]-1),fill=255)
for occ in occluders:
ob=to_png(occ,output)
if ob.width and ob.height:draw.rectangle((ob.x,ob.y,ob.end[0]-1,ob.end[1]-1),fill=0)
actual=Image.new('L',im.size);actual.putdata([255 if px==COLORS[target] else 0 for px in im.get_flattened_data()])
require(ImageChops.difference(expected,actual).getbbox() is None,'replay-paint-'+target)
return dict(count=sum(actual.histogram()[1:]),bbox=actual.getbbox())

View file

@ -0,0 +1,16 @@
--- a/nested-client.c
+++ b/nested-client.c
@@ -205,7 +205,12 @@
int main(int argc,char **argv) {
signal(SIGTERM,stop);
const char *placement=argc>1?argv[1]:"b_cross";
- if (!strcmp(placement,"visible")) {
+ /* EXPERIMENTAL: only placement changes; serial/grab/lifecycle stay historical.
+ * Both 1x1 anchors lie inside their parent SHM window geometry. */
+ if (!strcmp(placement,"static_cross")) {
+ a.anchor_x=100; a.anchor_y=80; a.width=350;
+ b.anchor_x=100; b.anchor_y=60; b.width=300;
+ } else if (!strcmp(placement,"visible")) {
a.anchor_x=50; a.anchor_y=80; a.width=250;
b.anchor_x=20; b.anchor_y=60; b.width=170;
} else if (!strcmp(placement,"both_cross")) {

View file

@ -0,0 +1,199 @@
"""Shared offline/live predicates: facts precede scientific classification.
CONTRACT: full RGB comparisons have no mask/tolerance; grabs require real logs.
INVARIANT: dismissal, client destruction, clipping and layout remain distinct.
"""
import re
from model import Rect,Space,Provenance,Output,popup,crossing,local_clip_to_global,require
from pixels import color_geometry,COLORS
from PIL import Image,ImageChops
class Defect(RuntimeError):
"""A directly measured scientific contract failure, distinct from fixture ambiguity."""
def paint(im,target):
im=im.convert('RGB');assert im.size==(800,600)
mask=Image.new('L',im.size);mask.putdata([255 if p==COLORS[target] else 0 for p in im.get_flattened_data()])
return dict(count=sum(mask.histogram()[1:]),bbox=mask.getbbox())
def point(im,target,origin):
box=paint(im,target)['bbox'];assert box,('no measured paint',target)
# WHY: A may be occluded by B; bbox center alone is not a valid hit point.
x1,y1,x2,y2=box
for y in range(y1+10,y2-10,5):
for x in range(x1+10,x2-10,5):
if all(im.getpixel((xx,yy))==COLORS[target] for yy in range(y-8,y+9) for xx in range(x-8,x+9)):
return [x+origin,y]
raise AssertionError('no solid measured interior '+target)
def equal(a,b):
assert a.size==b.size==(800,600)
rows=[(i%800,i//800,x,y) for i,(x,y) in enumerate(zip(a.get_flattened_data(),b.get_flattened_data())) if x!=y]
return dict(equal=not rows,changed=len(rows),bbox=ImageChops.difference(a,b).getbbox(),pixels=rows)
def reference(a,b):
result=equal(a,b)
assert result['equal'] and all(c==(48,48,56) for c in a.get_flattened_data()),'unstable reference'
return result
def configured(text,name):
rows=re.findall(rf'{name} ROLE_CONFIGURE x=(-?\d+) y=(-?\d+) w=(\d+) h=(\d+)',text)
assert rows,(name,'no configure')
return list(map(int,rows[-1]))
def geometry(text,origin,provenance=None):
a=configured(text,'POPUP_A');b=configured(text,'POPUP_B')
require(provenance is not None,'popup-owner-provenance-required')
p=provenance
top=Rect(Space.GLOBAL,*origin,0,0,p)
ids={n:list(map(int,re.search(rf'{n} CREATE wl=(\d+) xdg=(\d+) role=(\d+)',text).groups())) for n in ('TOPLEVEL','POPUP_A','POPUP_B')}
result={}
parent=top
for key,name,parent_name,c in [('A','POPUP_A','TOPLEVEL',a),('B','POPUP_B','POPUP_A',b)]:
parent_id=int(re.search(rf'{name} CREATE .*parent_xdg=(\d+)',text)[1])
ack=int(re.findall(rf'{name} XDG_CONFIGURE serial=(\d+) ack',text)[-1])
parent=popup(parent,Rect(Space.POPUP,*c,p),parent_id,ids[parent_name][1],ack,name+' MAP ' in text)
result[key]=parent.values()
result.update(configured_A=a,configured_B=b,origin=origin,provenance=dict(owner=p.owner,workspace=p.workspace,generation=p.generation,evidence=p.evidence,state=p.state),
crossing={key:crossing(Rect(Space.GLOBAL,*result[key],p),0) for key in ('A','B')})
return result
def mapped(text):
for name in ['POPUP_A','POPUP_B']:
assert text.count(name+' MAP ')==1 and name+' POPUP_DONE ' not in text and name+' DESTROY ' not in text,(name,'not mapped')
def protocol(text):
assert not re.search(r'wl_display[^\n]*\.error\(|protocol error|invalid_popup_parent|not_the_topmost_popup',text,re.I),'protocol error'
mapped(text)
ids={}
for name in ['TOPLEVEL','POPUP_A','POPUP_B']:
m=re.search(rf'{name} CREATE wl=(\d+) xdg=(\d+) role=(\d+)',text);assert m
ids[name]=list(map(int,m.groups()))
assert len({n for v in ids.values() for n in v})==9,'object identities reused'
grabs=[]
for name,parent in [('POPUP_A','TOPLEVEL'),('POPUP_B','POPUP_A')]:
create=re.search(rf'{name} CREATE .*parent={parent} parent_xdg=(\d+)',text);assert create
assert int(create[1])==ids[parent][1], 'wrong XDG parent'
debug_parent=re.search(rf'xdg_surface#{ids[name][1]}\.get_popup\(new id xdg_popup#{ids[name][2]}, xdg_surface#{ids[parent][1]}, xdg_positioner#\d+\)',text)
require(debug_parent is not None,'debug-parent-request')
m=re.search(rf'{name} GRAB_REQUEST origin=wl_pointer.button target={parent} serial=(\d+) used=(\d+)',text);assert m
serial,used=map(int,m.groups());assert serial==used and 0<serial<=0xffffffff
button=f'POINTER_BUTTON target={parent} serial={serial} button=272 state=1'
assert text.index(button)<m.start(),'grab serial not from earlier button'
debug_button=re.search(rf'wl_pointer#\d+\.button\({serial}, \d+, 272, 1\)',text)
require(debug_button is not None and debug_button.start()<m.start(),'debug-real-button-serial')
role=text.index(name+' ROLE_CONFIGURE ');cfg=re.search(rf'{name} XDG_CONFIGURE serial=(\d+) ack',text);assert cfg
mp=text.index(name+' MAP ')
assert m.start()<role<cfg.start()<mp,'configure ACK map order'
popup_role=ids[name][2];xdg=ids[name][1];wl=ids[name][0]
# WAYLAND_DEBUG is independent corroboration, not just fixture claims.
request=re.search(rf'xdg_popup#{popup_role}\.grab\(wl_seat#\d+, {serial}\)',text);assert request
ack=re.search(rf'xdg_surface#{xdg}\.ack_configure\({cfg[1]}\)',text);assert ack
attach=re.search(rf'wl_surface#{wl}\.attach\(',text);assert attach
commits=list(re.finditer(rf'wl_surface#{wl}\.commit\(\)',text));assert len(commits)>=2
assert request.start()<commits[0].start()<role<ack.start()<attach.start()<commits[1].start()<mp
actual=configured(text,name)
require(re.search(rf'xdg_popup#{popup_role}\.configure\({actual[0]}, {actual[1]}, {actual[2]}, {actual[3]}\)',text) is not None,'debug-popup-configure')
require(re.search(rf'xdg_surface#{xdg}\.configure\({cfg[1]}\)',text) is not None,'debug-xdg-configure')
native_attach=re.search(rf'wl_surface#{wl}\.attach\(wl_buffer#(\d+), 0, 0\)',text[ack.start():mp])
require(native_attach is not None,'popup-native-attach')
native_buffer=int(native_attach[1])
native_create=re.search(rf'create_buffer\(new id wl_buffer#{native_buffer}, 0, {actual[2]}, {actual[3]}, {actual[2]*4}, 1\)',text[role:mp])
require(native_create is not None,'popup-native-configured-size')
if parent=='POPUP_A':assert text.index('POPUP_A MAP ')<text.index(button)
grabs.append(dict(popup=name,parent=parent,serial=serial,used=used,origin='wl_pointer.button',ids=ids[name],ack=int(cfg[1]),native_buffer=native_buffer,native_size=actual[2:]))
assert grabs[0]['serial']<grabs[1]['serial'], 'distinct ordered serials'
return dict(ids=ids,grabs=grabs,hierarchy='TOPLEVEL -> POPUP_A -> POPUP_B',status='PASS')
def pair(lines,target):
events=[]
for line in lines:
m=re.fullmatch(r'POINTER_BUTTON target=(\w+) serial=(\d+) button=(\d+) state=(\d+)',line);assert m
events.append([m[1],*map(int,m.groups()[1:])])
if len(events)!=2 or any(e[0]!=target for e in events) or [e[2:] for e in events]!=[[273,1],[273,0]]:
raise Defect('wrong actual button recipient/pair: '+str(events))
assert 0<events[0][1]<events[1][1]<=0xffffffff
return events
def dismissal(text,buttons):
if any('target=POPUP_A ' in b or 'target=POPUP_B ' in b for b in buttons):
raise Defect('invisible popup received actual button')
done=re.findall(r'(POPUP_[AB]) POPUP_DONE ',text)
destroyed=re.findall(r'(POPUP_[AB]) DESTROY ',text)
assert done==['POPUP_B','POPUP_A'] and destroyed==['POPUP_B','POPUP_A'],('dismissal order',done,destroyed)
return dict(done=done,destroyed=destroyed,invisible_buttons=buttons,status='PASS',meaning='outside dismissal distinct from invisible hit')
def root_clip(text,origin,mosaic,owner_id,start_ns,end_ns):
# Traces lack popup owner IDs. Correlate the only live root in a bounded
# owner-observed window; ambiguity is a fixture failure, never rows[-1].
owners=[s for s in text.splitlines() if 'PI_OWNER output=HEADLESS-1 ' in s and f' id={owner_id} ' in s and start_ns<=int(re.search(r'ns=(\d+)',s)[1])<=end_ns]
rows=[s for s in text.splitlines() if 'PI_POPUP output=HEADLESS-1 ' in s and start_ns<=int(re.search(r'ns=(\d+)',s)[1])<=end_ns]
require(bool(owners) and bool(rows),'bounded-root-owner-observations')
parsed=[]
for row in rows:
m=re.search(r'local_index=(\d+) tree=(\S+) enabled=(\d+) clip_valid=(\d+) clip=(-?\d+),(-?\d+),(\d+),(\d+)',row)
require(m is not None,'root-trace-format')
index,tree,enabled,valid,*box=m.groups()
parsed.append((int(index),tree,int(enabled),bool(int(valid)),tuple(map(int,box))))
require(len({r[1] for r in parsed})==1,'root-chain-unique')
require(len(set(parsed))==1,'root-window-state-consistent')
index,tree,enabled,valid,box=parsed[0]
require(index==1 and enabled==1,'root-enabled-index')
if valid!=mosaic:raise Defect('root clip state mismatch')
if mosaic:
p=Provenance(owner_id,1,'bounded-root-window','PI_OWNER + PI_POPUP')
global_clip=local_clip_to_global(Rect(Space.CONTENT,*box,p),origin,p)
require(global_clip.values()==[-800,0,800,600],'root-applied-global-clip')
return dict(tree=tree,clip_valid=valid,local=list(box),origin=origin,raw=rows[0],owner=owner_id,window=[start_ns,end_ns],correlation='unique root and bounded owner observation; no atomic generation claim',child='inherited source hierarchy')
def popup_pixels(left,right,g,mosaic,baseline):
# The runner and actual historical replay share exact typed mask conversion.
require('provenance' in g,'popup-paint-provenance')
p=Provenance(**g['provenance']);A=Rect(Space.GLOBAL,*g['A'],p);B=Rect(Space.GLOBAL,*g['B'],p)
clip=Rect(Space.VIEWPORT,-800,0,800,600,p) if mosaic else None
result={}
for side,im,ox in [('H1',left,-800),('H2',right,0)]:
output=Output(side,Rect(Space.GLOBAL,ox,0,800,600,p),1.0,'normal')
result[side]={name:color_geometry(im,name,r,output,clip,(B,) if name=='POPUP_A' else ()) for name,r in [('POPUP_A',A),('POPUP_B',B)]}
require(all(result['H1'][name]['count']>0 for name in ('POPUP_A','POPUP_B')),'permitted-popup-color')
if mosaic:
result['whole_H2']=equal(baseline,right)
if not result['whole_H2']['equal']:raise Defect('whole-H2 changed under Mosaic')
else:
require(all(result['H2'][name]['count']>0 for name in ('POPUP_A','POPUP_B')),'standard-popup-continuation')
return result
def terminal(measures,ipc_code,compositor_code,log,protocol_error,rescue,stdout='',stderr='',reaped=True):
ok=bool(measures and compositor_code==0 and "Handling command 'exit'" in log
and 'Shutting down sway' in log and not protocol_error and not rescue)
# Reaping is completed by the runner after recording actual terminal IPC.
require(type(ipc_code) is int and type(compositor_code) is int,'actual-terminal-codes')
return dict(scientific_cleanup_pass=ok,ipc_exit=ipc_code,compositor_exit=compositor_code,
stdout=stdout,stderr=stderr,all_owned_reaped=reaped,ipc_success=ipc_code==0,transport_incident=bool(ok and ipc_code!=0),
interpretation=('compatible queued-response loss, not proven packet causality' if ok and ipc_code!=0 else 'actual recorded IPC outcome'))
def terminal_exchange(execute, wait, argv, env, measures, compositor_log,
protocol_error, rescue, record):
"""CONTRACT: preserve an obtained IPC reply before fallible compositor wait."""
data=dict(scientific_cleanup_pass=False,ipc_exit=None,stdout='',stderr='',
compositor_exit=None,measurements_completed=measures)
try:
reply=execute(argv,env=env,capture_output=True,text=True,timeout=3)
data.update(ipc_exit=reply.returncode,stdout=reply.stdout,stderr=reply.stderr)
record(reply.stdout,reply.stderr)
except Exception as exc:
data['ipc_error']=repr(exc)
return data
try:
data['compositor_exit']=wait(timeout=3)
except Exception as exc:
data['compositor_error']=repr(exc)
return data
try:
data.update(terminal(measures,data['ipc_exit'],data['compositor_exit'],
compositor_log(),protocol_error(),rescue(),stdout=data['stdout'],
stderr=data['stderr'],reaped=False))
except Exception as exc:
data['terminal_error']=repr(exc)
return data

View file

@ -0,0 +1,51 @@
#!/usr/bin/env python3
"""Compile-only C17 clients/protocols outside Git. Never execute any client."""
import argparse
import json
from pathlib import Path
import shutil
import subprocess
from support import sha,save,environment
from model import require
HERE=Path(__file__).resolve().parent
PROBES=HERE.parent
def prepare(lab):
dest=lab/'client-build';dest.mkdir(exist_ok=True)
raw=lab/'raw'
commands=[]
def command(label,args):
result=subprocess.run(list(map(str,args)),cwd=dest,env=environment(),text=True,capture_output=True,timeout=30)
(raw/(label+'.stdout')).write_text(result.stdout);(raw/(label+'.stderr')).write_text(result.stderr)
commands.append(dict(label=label,argv=list(map(str,args)),exit=result.returncode))
require(result.returncode==0,'client-preparation-'+label)
return result.stdout
contract=json.loads((HERE/'client-contract.json').read_text())
inputs={}
for name,source in [('nested-client.c',PROBES/'step20c-nested-grab/nested-client.c'),('pointer-daemon.c',PROBES/'step20c-valid-grab/pointer-daemon.c'),('static-reference.c',PROBES/'step20c-saved-target-timeout-input/static-reference.c'),('saved-client.c',PROBES/'step20c-saved-target-timeout-input/saved-client.c')]:
shutil.copyfile(source,dest/name);inputs[str(source)]=sha(source)
require(inputs[str(PROBES/'step20c-nested-grab/nested-client.c')]=='2e40c98af72a0df8b316810589a0be8f4425a763db1de448b49a7813956b6f7d','frozen-nested-source')
command('placement-check',['git','apply','--check',HERE/'placement.patch'])
command('placement-apply',['git','apply',HERE/'placement.patch'])
prior=PROBES/'step20c-static-nested-grab/placement.patch'
require(sha(prior)==sha(HERE/'placement.patch'),'byte-identical-placement')
require(sha(dest/'nested-client.c')==contract['adapted_nested_sha256'],'byte-identical-adapted-client')
protocols={}
for stem,xml in [('xdg-shell',Path('/usr/share/wayland-protocols/stable/xdg-shell/xdg-shell.xml')),('virtual-pointer',PROBES/'step20c-valid-grab/wlr-virtual-pointer-unstable-v1.xml')]:
for mode,suffix in [('client-header','-client.h'),('private-code','-protocol.c')]:
path=dest/(stem+suffix);command(stem+'-'+mode,['wayland-scanner',mode,xml,path])
require(sha(path)==contract['protocols'][path.name],'byte-identical-protocol-'+path.name)
protocols[path.name]=sha(path)
flags=command('wayland-flags',['pkg-config','--cflags','--libs','wayland-client']).split()
builds=[]
for name,stem in [('nested-client','xdg-shell'),('pointer-daemon','virtual-pointer'),('static-reference','xdg-shell')]:
args=['cc','-std=c17','-Wall','-Wextra','-Werror','-Wno-unused-parameter','-I'+str(dest),dest/(name+'.c'),dest/(stem+'-protocol.c'),*flags]
command(name+'-syntax',args+['-fsyntax-only']);command(name+'-compile',args+['-o',dest/name])
builds.append(dict(client=name,source=sha(dest/(name+'.c')),binary=sha(dest/name),execution='NOT RUN'))
save(lab,'client-provenance',dict(status='PASS C17 -Werror syntax/build; clients NOT RUN',inputs=inputs,patch=sha(HERE/'placement.patch'),adapted_nested=sha(dest/'nested-client.c'),protocols=protocols,protocol_comparison='byte-identical historical exact sources',builds=builds,commands=commands))
print('Client-only C17 preparation PASS; no client execution')
if __name__=='__main__':
parser=argparse.ArgumentParser();parser.add_argument('lab',type=Path);prepare(parser.parse_args().lab)

View file

@ -0,0 +1,226 @@
#!/usr/bin/env python3
"""Read-only historical input replay. Writes JSON only in the new offline LAB."""
import argparse
import json
from pathlib import Path
import re
from PIL import Image
from model import *
from observations import applied_model,output_model,viewport_model
from predicates import COLORS,paint,protocol,pair,dismissal,equal,reference
from ipc_predicates import nodes,validate_reference
from support import save,sha
from pixels import color_geometry
HISTORICAL = Path('/home/fy59/swayfx-mosaic-static-nested-grab-m0a5e2qh')
NESTED = Path('/tmp/swayfx-mosaic-nested-grab-If8ofeUu')
def correlate_historical(text,injections,rects,standard=None):
"""CONTRACT: wire button times bind actions; map retarget uses the last point.
WHY: callbacks have no injection timestamp of their own. Pre-injection seat
events remain explicitly unpaired; software motion retains its wire time.
"""
actions=[];stamp=1000
for kind,x,y in re.findall(r'^INJECT (left|right|move) (-?\d+),(-?\d+)$',injections,re.M):
action=dict(index=len(actions),kind=kind,global_point=[int(x),int(y)],motion_msec=stamp)
stamp+=1
if kind!='move':
action.update(press_msec=stamp,release_msec=stamp+1,button=272 if kind=='left' else 273);stamp+=2
actions.append(action)
require(bool(actions),'historical-injections-present')
bytime={a[k]:a for a in actions for k in ('motion_msec','press_msec','release_msec') if k in a}
lines=text.splitlines();callbacks=[];events=[];current=actions[0];locations={};phase='opening';wire=None;standard_active=False;live=set()
firstpress=next(i for i,l in enumerate(lines) if re.search(r'wl_pointer#\d+\.button\(\d+, 1001,',l))
initialenter=max(i for i,l in enumerate(lines[:firstpress]) if l.startswith('POINTER_ENTER '))
identities={n:int(v) for n,v in re.findall(r'^(TOPLEVEL|POPUP_A|POPUP_B) CREATE wl=(\d+)',text,re.M)}
for i,line in enumerate(lines):
lifecycle=re.match(r'(TOPLEVEL|POPUP_A|POPUP_B) (MAP|DESTROY) ',line)
if lifecycle:
if lifecycle[2]=='MAP':live.add(lifecycle[1])
else:live.discard(lifecycle[1])
if standard and line.startswith('TOPLEVEL ROLE_CONFIGURE ') and 'POPUP_B MAP ' in '\n'.join(lines[:i]):standard_active=True;phase='standard'
if line.startswith('COMMAND close_b DONE'):phase='after-B-close'
if line.startswith('POPUP_B MAP '):phase='mapped'
debug=re.search(r'wl_pointer#\d+\.(button|motion|enter)\(([^)]+)\)',line)
if debug:
wire=(debug[1],[v.strip() for v in debug[2].split(',')])
if wire[0]!='enter':
time=int(wire[1][1] if wire[0]=='button' else wire[1][0])
if time in bytime:current=bytime[time]
match=re.match(r'POINTER_(ENTER|MOTION) target=(\w+) (?:wl=\d+ serial=\d+ )?x=([\d.-]+) y=([\d.-]+)',line)
active=standard if standard_active else rects
if match:
kind,target,x,y=match.groups();local=[float(x),float(y)]
record=dict(line=i+1,kind=kind,target=target,local=local,phase=phase)
if i<initialenter:
record.update(status='NOT AVAILABLE / NOT REPLAYED',scope='seat event before first identifiable injected enter')
callbacks.append(record);continue
require(target in active and target in live,'historical-pointer-recipient')
require(wire is not None and wire[0]==kind.lower(),'historical-coordinate-wire-kind')
offset=2 if kind=='ENTER' else 1
require(local==list(map(float,wire[1][offset:offset+2])),'historical-coordinate-wire-local')
if kind=='ENTER':
require(int(re.search(r'#(\d+)',wire[1][1])[1])==identities[target],'historical-enter-surface-identity')
if kind=='ENTER':
# INVARIANT: a motion before the next wire button means this enter
# belongs to the previous point (automatic mapping retarget).
following=next((j for j in range(i+1,len(lines)) if re.search(r'wl_pointer#\d+\.(button|motion)\(',lines[j])),None)
if following is not None and '.button(' in lines[following]:
t=int(re.search(r'\.button\(\d+, (\d+),',lines[following])[1]);current=bytime.get(t,current)
pointer_local(current['global_point'],active[target],local)
locations[target]=local
record.update(status='PASS',action=current['index'],global_point=current['global_point'],origin=[active[target].x,active[target].y],wire=wire)
callbacks.append(record)
button=re.match(r'POINTER_BUTTON target=(\w+) serial=(\d+) button=(\d+) state=(\d+)',line)
if button:
target,serial,key,state=button.groups();serial,key,state=map(int,(serial,key,state))
require(wire is not None and wire[0]=='button','historical-button-wire-present')
ws,tm,wk,st=map(int,wire[1]);require((serial,key,state)==(ws,wk,st),'historical-button-wire-identity')
require(tm in bytime,'historical-button-injection-time')
action=bytime[tm];require(tm==action.get('press_msec' if state else 'release_msec') and key==action.get('button'),'historical-button-action-order')
require(target in active and target in live and target in locations,'historical-pointer-recipient')
pointer_local(action['global_point'],active[target],locations[target])
events.append(dict(line=i+1,target=target,serial=serial,button=key,state=state,msec=tm,action=action['index'],phase=phase,raw=line))
wire=None
require(len(events)>=4,'historical-opening-buttons')
require([e['target'] for e in events[:4]]==['TOPLEVEL','TOPLEVEL','POPUP_A','POPUP_A'],'historical-opening-recipients')
times=[e['msec'] for e in events];require(times==sorted(set(times)),'historical-button-sequence')
paired={e['action'] for e in events}
for index in paired:
group=[e for e in events if e['action']==index]
require(len(group)==2 and [e['state'] for e in group]==[1,0] and group[0]['target']==group[1]['target'],'historical-button-complete-pair')
if 'POPUP_B POPUP_DONE ' in text:
forbidden=actions[-1]
require(forbidden['index'] not in paired,'historical-forbidden-button-delivery')
else:
require(paired=={a['index'] for a in actions if a['kind']!='move'},'historical-required-visible-buttons')
return dict(status='PASS',actions=actions,callbacks=callbacks,buttons=events,
forbidden_buttons=[e['raw'] for e in events if e['action']==actions[-1]['index']] if 'POPUP_B POPUP_DONE ' in text else [])
def replay_native(lab,historical=HISTORICAL):
cal=json.loads((historical/'results/camera-calibration.json').read_text())[-1]
snap=json.loads((historical/'results/E1-applied-snapshot.json').read_text())
client=(historical/'run/E1.log').read_text()
measured={**cal['after_owner'],'workspace':cal['scene']['workspace']}
owner=measured['IPC']
applied=applied_model(measured,owner,client,'historical-E1-applied')
rect=content(applied);out=output_model(snap,'HEADLESS-1',rect.provenance)
clip=viewport_model(cal['scene'],rect.provenance)
require(measured['raw'] in (historical/'run/compositor.log').read_text(),'historical-applied-trace')
value=paint(Image.open(historical/'run/E1-top.png'),'TOPLEVEL')
png=verify_paint(rect,out,value['bbox'],value['count'],clip)
require((applied.native.rectangle.width,applied.native.rectangle.height)==(420,320),'historical-shm')
require((rect.width,rect.height)==(636,573) and (rect.x,rect.y)==(-318,25),'historical-render')
require(value==dict(bbox=(482,25,800,598),count=182214),'historical-paint')
require(png.height!=applied.native.rectangle.height and rect.y!=applied.scene.y+applied.window.y,'reproduce-two-invalid-assumptions')
validate_reference(snap,cal['reference']['con_id'],cal['reference']['pid'])
reference(Image.open(historical/'run/H2-reference-1.png').convert('RGB'),Image.open(historical/'run/H2-reference-2.png').convert('RGB'))
records={
'native-shm':dict(status='PASS',buffer=applied.native.buffer_id,size=applied.native.rectangle.values(),stride=applied.native.stride,format=applied.native.format,source=str(historical/'run/E1.log'),PNG_identity='NOT PROVEN'),
'xdg-configure':dict(status='PASS',toplevel=applied.configured.values(),initial_ACK=applied.native.commit_serial,assigned_ACK=applied.configure_ack,initial_configure=[0,0],new_buffer_after_assigned_configure=False,popups='NOT EXERCISED'),
'applied':dict(status='PASS',owner=owner['id'],pid=owner['pid'],workspace=rect.provenance.workspace,scene=applied.scene.values(),window=applied.window.values(),titlebar=applied.titlebar,scroll=cal['after'],globalclip=clip.values(),generation='atomic transaction identity NOT TESTED'),
'rendered':dict(status='PASS',content=rect.values(),PNG_bbox=value['bbox'],count=value['count'],visible_intersection=png.values(),native_equals_dest=False),
'historical-evidence':dict(status='PASS read-only historical replay',inputs={str(historical/'run'/n):sha(historical/'run'/n) for n in ('E1.log','E1-top.png','compositor.log')},diagnostic=str(historical/'results/geometry-fixture-diagnostic.json'),runtime='INCONCLUSIVE / no popup / no grab')}
for name,data in records.items():save(lab,name,data)
return records
def replay_nested(lab,root=NESTED):
results=[]
dirs=('run-private_mosaic-crossing-b_cross','run-private_mosaic-crossing-both_cross',
'run-private_mosaic-toggle-b_cross','run-private_mosaic-outside-visible',
'run-control-crossing-b_cross','run-control-crossing-both_cross','run-control-outside-visible',
'run-private_mosaic-close_b-visible','run-control-close_b-visible')
for dirname in dirs:
directory=root/dirname
if not directory.is_dir():
results.append(dict(case=dirname,status='NOT AVAILABLE'));continue
text=(directory/'client.log').read_text()
stop=min([m.start() for m in re.finditer(r'POPUP_[AB] (?:POPUP_DONE|DESTROY)',text)] or [len(text)])
opened=text[:stop]
prot=protocol(opened)
tree=json.loads((directory/'tree-open.json').read_text())
ws=next(n for n in nodes(tree) if n.get('type')=='workspace' and n.get('name')=='1')
owner=next(n for n in nodes(ws) if n.get('app_id')=='org.mosaic.NestedGrabProbe')
prov=Provenance(owner['id'],ws['id'],dirname+'-open','IPC + clip + RGB; no atomic generation')
comp=(directory/'compositor.log').read_text()
clips=re.findall(r'PROBE_POPUP_CLIP owner=(\S+) local=(-?\d+),(-?\d+) (\d+)x(\d+)',comp)
private='private_mosaic' in dirname
if private:
require(bool(clips),'historical-popup-root-clip')
require(len({c[0] for c in clips})==1,'historical-unique-owner-pointer')
_,cx,cy,cw,ch=clips[0];origin=(-int(cx),-int(cy))
clip=Rect(Space.VIEWPORT,0,0,int(cw),int(ch),prov)
require(origin==(owner['rect']['x']-int(ws['mosaic']['rows'][0]['scroll_x'])+owner['window_rect']['x'],owner['deco_rect']['height']+owner['window_rect']['y']),'historical-origin-corroboration')
else:
origin=(owner['rect']['x']+owner['window_rect']['x'],owner['deco_rect']['height']+owner['window_rect']['y']);clip=None
top=Rect(Space.GLOBAL,*origin,owner['window_rect']['width'],owner['window_rect']['height'],prov)
configs={n:list(map(int,re.findall(rf'{n} ROLE_CONFIGURE x=(-?\d+) y=(-?\d+) w=(\d+) h=(\d+)',opened)[-1])) for n in ('POPUP_A','POPUP_B')}
A=popup(top,Rect(Space.POPUP,*configs['POPUP_A'],prov),prot['ids']['TOPLEVEL'][1],prot['ids']['TOPLEVEL'][1],prot['grabs'][0]['ack'],True)
B=popup(A,Rect(Space.POPUP,*configs['POPUP_B'],prov),prot['ids']['POPUP_A'][1],prot['ids']['POPUP_A'][1],prot['grabs'][1]['ack'],True)
outputs=json.loads((directory/'outputs-open.json').read_text())
colors={}
for side,name in (('left','HEADLESS-1'),('right','HEADLESS-2')):
out=output_model({'outputs':outputs},name,prov)
im=Image.open(directory/(side+'-open.png')).convert('RGB')
colors[side]={n:color_geometry(im,n,r,out,clip,(B,) if n=='POPUP_A' else ()) for n,r in (('POPUP_A',A),('POPUP_B',B))}
pointers=re.findall(r'POINTER_(ENTER|MOTION) target=(\w+) (?:wl=\d+ serial=\d+ )?x=([\d.-]+) y=([\d.-]+)',text)
injections=(directory/'pointer.log').read_text()
buttons=[line for line in text.splitlines() if line.startswith('POINTER_BUTTON ')]
done=re.findall(r'(POPUP_[AB]) POPUP_DONE ',text)
destroyed=re.findall(r'(POPUP_[AB]) DESTROY ',text)
row=dict(case=dirname,status='PASS historical sampled replay',owner=owner['id'],pid=owner['pid'],workspace=ws['id'],scroll=ws.get('mosaic',{}).get('rows',[{}])[0].get('scroll_x'),origin=origin,A=A.values(),B=B.values(),configured=configs,protocol=prot,clip=clip.values() if clip else None,colors=colors,pointer_callbacks=pointers,pointer_injections=injections.splitlines(),buttons=buttons,done=done,destroyed=destroyed,files={p.name:sha(p) for p in directory.iterdir() if p.is_file()},native_frame_identity='NOT PROVEN')
require(destroyed==['POPUP_B','POPUP_A'],'historical-child-first-destruction')
if 'toggle' in dirname:
stdtree=json.loads((directory/'tree-standard.json').read_text());stdws=next(n for n in nodes(stdtree) if n.get('id')==ws['id']);stdowner=next(n for n in nodes(stdws) if n.get('id')==owner['id'])
require(stdws['layout']=='splith' and not done,'historical-standard-mapped')
sp=Provenance(owner['id'],ws['id'],dirname+'-standard','fresh standard IPC + paint')
so=(stdowner['rect']['x']+stdowner['window_rect']['x'],stdowner['deco_rect']['height']+stdowner['window_rect']['y'])
stdtop=Rect(Space.GLOBAL,*so,stdowner['window_rect']['width'],stdowner['window_rect']['height'],sp)
stdA=Rect(Space.GLOBAL,so[0]+configs['POPUP_A'][0],so[1]+configs['POPUP_A'][1],*configs['POPUP_A'][2:],sp)
stdB=Rect(Space.GLOBAL,stdA.x+configs['POPUP_B'][0],stdA.y+configs['POPUP_B'][1],*configs['POPUP_B'][2:],sp)
fresh_standard(top,stdtop)
stdcolors={}
stdoutputs=json.loads((directory/'outputs-standard.json').read_text())
for side,name in (('left','HEADLESS-1'),('right','HEADLESS-2')):
im=Image.open(directory/(side+'-standard.png')).convert('RGB');out=output_model({'outputs':stdoutputs},name,sp)
stdcolors[side]={n:color_geometry(im,n,r,out,None,(stdB,) if n=='POPUP_A' else ()) for n,r in (('POPUP_A',stdA),('POPUP_B',stdB))}
row['standard']=dict(origin=so,A=stdA.values(),B=stdB.values(),colors=stdcolors,buttons=pair([b for b in buttons if 'target=POPUP_B ' in b],'POPUP_B'),root_clip_clear='source + pixels; no explicit clear trace NOT PROVEN',A_survived_explicit_B_close='NOT REPLAYED')
standard_rects={'TOPLEVEL':stdtop,'POPUP_A':stdA,'POPUP_B':stdB}
elif 'close_b' in dirname:
require('COMMAND close_b DONE' in text and not done,'historical-explicit-B-close')
closepos=text.index('COMMAND close_b DONE')
require(text.index('POPUP_B DESTROY ')<closepos<text.index('POPUP_A DESTROY '),'historical-A-survives-B-close')
Aevents=[b for b in text[closepos:].splitlines() if b.startswith('POINTER_BUTTON ')]
row['explicit_B_close']=dict(status='PASS historical',A_buttons=pair(Aevents,'POPUP_A'),A_mapped_until_owner_close=True,B_reopened=False)
require(text.count('POPUP_B MAP ')==1,'historical-no-B-reopen')
closecolors={}
for side,name in (('left','HEADLESS-1'),('right','HEADLESS-2')):
im=Image.open(directory/(side+'-closed-b.png')).convert('RGB');out=output_model({'outputs':outputs},name,prov)
closecolors[side]=color_geometry(im,'POPUP_A',A,out,clip)
require(paint(im,'POPUP_B')['count']==0,'historical-B-color-removed')
row['explicit_B_close']['colors']=closecolors
elif done:
start=text.index('POPUP_B POPUP_DONE ')
# CONTRACT: earlier visible buttons are distinct from the final
# forbidden action; all observed events remain in the correlation.
correlation=correlate_historical(text,injections,{'TOPLEVEL':top,'POPUP_A':A,'POPUP_B':B})
row['dismissal']=dismissal(text[start:],correlation['forbidden_buttons'])
row['visible_buttons_before_forbidden_action']=[e for e in correlation['buttons'] if e['action']<correlation['actions'][-1]['index']]
row['input_correlation']=correlate_historical(text,injections,{'TOPLEVEL':top,'POPUP_A':A,'POPUP_B':B},standard_rects if 'toggle' in dirname else None)
results.append(row)
save(lab,'historical-replay',dict(status='PASS sampled historical facts',cases=results,missing={'new-static-popups':'NOT REPLAYED','atomic-generation':'NOT TESTED','new-standard-A-after-B-close':'NOT REPLAYED'}))
save(lab,'popup-root',{'status':'PASS historical replay','cases':[{k:r.get(k) for k in ('case','origin','A','clip')} for r in results]})
save(lab,'popup-nested',{'status':'PASS historical replay','cases':[{k:r.get(k) for k in ('case','B','protocol','standard','dismissal')} for r in results]})
return results
def main():
p=argparse.ArgumentParser();p.add_argument('lab',type=Path);args=p.parse_args()
replay_native(args.lab);replay_nested(args.lab)
save(args.lab,'positioner',dict(status='PASS source-backed prediction',flags=0,A=[100,80,350,170],B=[100,60,300,130],predicted_content_origin=[-318,25],predicted_A=[-218,105,350,170],predicted_B=[-118,165,300,130],runtime='NOT TESTED; actual configure/ACK/map required'))
print('Historical geometry replays PASS; new runtime NOT TESTED')
if __name__=='__main__':main()

View file

@ -0,0 +1,345 @@
#!/usr/bin/env python3
"""One immutable-static headless process, two genuinely grabbed XDG chains.
WHY: outside dismissal must not preclude standard-return measurements.
CONTRACT: every mutation/injection/capture consumes a persistent reservation.
INVARIANT: only owned groups/sockets; actual codes survive terminal IPC failure.
"""
import argparse
import fcntl
import json
import os
from pathlib import Path
import re
import shutil
import signal
import subprocess
import tempfile
import threading
import time
from PIL import Image
from support import sha,save,reserve,environment,verify
from model import *
from authorization import authorize
from observations import applied_model,output_model,viewport_model,verify_owner_occlusion
from ipc_predicates import nodes,workspace,validate_outputs,validate_reference,measure_owner,scene_from_log,validate_camera
from predicates import Defect,COLORS,paint,point,equal,reference,protocol,geometry,mapped,pair,dismissal,root_clip,popup_pixels,terminal,terminal_exchange
p=argparse.ArgumentParser();p.add_argument('lab',type=Path);p.add_argument('--future-authorization',type=Path)
args=p.parse_args();lab=args.lab.resolve()
# Fail CLOSED before owner/lock/ledger/runtime creation or any subprocess.
auth=authorize(lab,args.future_authorization)
OWNER=Path(auth['owner_registry']);BINARY=Path(auth['binary']);BINARY_SHA=auth['binary_sha256'];WLROOTS_SHA=auth['wlroots_sha256']
require(not __import__('sys').flags.optimize,'assertions required')
assert OWNER.read_text().strip()==str(lab) and (lab/'campaign-owner').read_text().strip()==str(OWNER)
lock=(lab/'run.lock').open('a+');fcntl.flock(lock,fcntl.LOCK_EX|fcntl.LOCK_NB)
freeze=verify(lab/'results/fixture-freeze-sha256.txt');gate=json.loads((lab/'results/offline-gate.json').read_text())
assert gate['marker']=='SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE=READY_FOR_NEW_RUNTIME' and gate['fixture_sha256']==freeze['sha256']
assert json.loads((lab/'results/binary-identity.json').read_text())['status']=='PASS'
assert sha(BINARY)==sha(lab/'swayfx-mosaic')==BINARY_SHA
assert not (lab/'run').exists(),'run path already used'
reserve(lab,'run')
run=lab/'run';run.mkdir();runtime=Path(tempfile.mkdtemp(prefix='msng-',dir='/tmp'));runtime.chmod(0o700)
assert len(os.fsencode(str(runtime/'sway-ipc.4294967295.2147483647.sock')))<108
(run/'runtime-path').write_text(str(runtime)+'\n')
config='output HEADLESS-1 resolution 800x600 scale 1 transform normal position -800 0\noutput HEADLESS-2 resolution 800x600 scale 1 transform normal position 0 0\nworkspace 1 output HEADLESS-1\nworkspace 2 output HEADLESS-2\nfocus_follows_mouse no\nseat seat0 hide_cursor 100\n'
(run/'config').write_text(config)
env=environment();env.update(XDG_RUNTIME_DIR=str(runtime),WLR_BACKENDS='headless',WLR_HEADLESS_OUTPUTS='2',WLR_RENDERER='pixman')
processes=[];files=[];comp=None;pointer=None;failure=None;stage='startup';measures=False;rescue=False
started=time.monotonic();finished=threading.Event();expired=threading.Event();chains={};clips={};root_boundary={};captures=[];clicks=[];owners={};camera_rows=[]
def event(kind,**data):
with (run/'events.jsonl').open('a') as out:out.write(json.dumps(dict(ns=time.monotonic_ns(),kind=kind,**data))+'\n')
def spawn(name,argv,debug=False):
assert not expired.is_set()
out=(run/(name+'.log')).open('w');files.append(out)
proc=subprocess.Popen(list(map(str,argv)),stdin=subprocess.PIPE,stdout=out,stderr=subprocess.STDOUT,
text=True,start_new_session=True,env={**env,**({'WAYLAND_DEBUG':'1'} if debug else {})})
processes.append((name,proc));event('spawn',name=name,pid=proc.pid,argv=list(map(str,argv)));return proc
def stop_owned(sig=signal.SIGTERM):
for name,proc in list(processes):
try:os.killpg(proc.pid,sig)
except ProcessLookupError:pass
def watchdog():
while not finished.wait(.1):
if time.monotonic()-started>150 or any(p.stat().st_size>32*1024*1024 for p in run.glob('*.log')):
expired.set();stop_owned();return
thread=threading.Thread(target=watchdog,daemon=True);thread.start()
def log(name):return (run/(name+'.log')).read_text(errors='replace')
def wait(fn,seconds=6):
end=min(time.monotonic()+seconds,started+143)
while time.monotonic()<end:
if expired.is_set():raise RuntimeError('deadline/log bound exceeded')
if comp is not None and comp.poll() is not None:raise RuntimeError('unexpected compositor exit '+str(comp.returncode))
value=fn()
if value:return value
time.sleep(.025)
raise RuntimeError('fixture wait timeout at '+stage)
def ipc(*args):
assert sock.is_relative_to(runtime) and sock.is_socket()
r=subprocess.run(['swaymsg','-s',str(sock),*args],env=env,capture_output=True,text=True,timeout=4)
event('ipc',args=args,exit=r.returncode,stdout=r.stdout,stderr=r.stderr)
assert r.returncode==0,('IPC failure',args,r.returncode)
return json.loads(r.stdout)
def cmd(text):
assert all(x['success'] for x in ipc(text)),text
def snapshot(tag):
tree=ipc('-t','get_tree');outputs=ipc('-t','get_outputs');ws=ipc('-t','get_workspaces')
data=dict(ns=time.monotonic_ns(),tree=tree,outputs=outputs,workspaces=ws,focused=[n['id'] for n in nodes(tree) if n.get('focused')])
save(lab,tag+'-snapshot',data);return data
def find(app,pid):
candidates=[n for n in nodes(ipc('-t','get_tree')) if n.get('app_id')==app and n.get('pid')==pid]
assert len(candidates)<=1
return candidates[0] if candidates else None
def capture(tag,output):
reserve(lab,'capture');time.sleep(.20)
path=run/(tag+'.png');assert not path.exists()
before=time.monotonic_ns()
r=subprocess.run(['grim','-s','1','-o',output,str(path)],env=env,capture_output=True,text=True,timeout=4)
event('capture',file=path.name,output=output,start_ns=before,exit=r.returncode,stderr=r.stderr)
assert r.returncode==0
im=Image.open(path).convert('RGB');assert im.size==(800,600)
captures.append(dict(file=path.name,output=output,sha256=sha(path),ns=time.monotonic_ns()))
save(lab,'captures',captures);return im
def inject(action,xy,grab=False):
assert action in ['left','right','move'] and len(xy)==2
x,y=xy;assert type(x) is int and type(y) is int and -800<=x<800 and 0<=y<600
kinds=['move'] if action=='move' else ['click','move']+(['grab'] if grab else [])
reserve(lab,*kinds)
marker=f'INJECT_DONE {action} {x+800},{y}';before=log('pointer').count(marker)
pointer.stdin.write(f'{action} {x+800} {y}\n');pointer.stdin.flush()
wait(lambda:log('pointer').count(marker)>before);time.sleep(.18)
event('injection',action=action,global_point=xy,sent=[x+800,y],extent=[1600,600],grab=grab)
def buttons(name):
return [s for s in log(name).splitlines() if s.startswith(('POINTER_BUTTON ','BUTTON '))]
def click(tag,name,xy,grab=False,action='right'):
before={n:len(buttons(n)) for n in [name,'reference','filler']}
t0=time.monotonic_ns();inject(action,xy,grab)
row=dict(tag=tag,global_point=xy,action=action,start_ns=t0,end_ns=time.monotonic_ns(),events={n:buttons(n)[before[n]:] for n in before})
clicks.append(row);save(lab,'clicks',clicks);return row
def delivery(row,name,target):
assert not row['events']['reference'] and not row['events']['filler'],'other client received visible popup button'
return pair(row['events'][name],target)
def correlate_pointer(name,xy,rect,target):
# WHY: an injection request alone does not identify applied popup origin.
rows=re.findall(rf'POINTER_(?:ENTER|MOTION) target={target} .*?x=([\d.-]+) y=([\d.-]+)',log(name))
assert rows,'missing pointer local coordinates'
local=list(map(float,rows[-1]));expected=[xy[0]-rect[0],xy[1]-rect[1]]
prov=Provenance(1,1,'pointer-sample','actual pointer log')
pointer_local(xy,Rect(Space.GLOBAL,*rect,prov),local)
return dict(global_point=xy,local=local,rectangle=rect)
def close_client(proc,name,value):
proc.stdin.write(value+'\n');proc.stdin.flush()
code=proc.wait(timeout=3);assert code==0,(name,code)
assert 'TOPLEVEL DESTROY' in log(name)
wait(lambda:find('org.mosaic.NestedGrabProbe',proc.pid) is None)
# CONTRACT: applied owner, paint and XDG surface size are distinct measurements.
def owner_state(name,proc,tag):
snap=snapshot(tag);ws=workspace(snap['tree'],'1');owner=next(n for n in nodes(ws) if n.get('pid')==proc.pid)
assert owner['app_id']=='org.mosaic.NestedGrabProbe' and owner['shell']=='xdg_shell' and owner['visible']
assert ws['output']=='HEADLESS-1' and owner['focused'] and snap['focused']==[owner['id']]
measured=measure_owner(log('compositor'),owner);scene=scene_from_log(log('compositor'),'HEADLESS-1')
assert scene['workspace']==ws['id']
measured['workspace']=ws['id']
return snap,ws,owner,measured,scene
def open_chain(name):
global stage
reserve(lab,'chain');cmd('workspace 1');proc=spawn(name,[lab/'nested-client','static_cross'],debug=True)
wait(lambda:find('org.mosaic.NestedGrabProbe',proc.pid) and 'TOPLEVEL MAP ' in log(name));time.sleep(.6)
snap,ws,owner,before,sc=owner_state(name,proc,name+'-before-camera')
assert ws['layout']=='mosaic'
current=ws['mosaic']['rows'][0]['scroll_x'];x,w=before['horizontal_content'];desired=-w//2;delta=int(x-desired)
if delta:
reserve(lab,'camera');cmd(f'[con_id={owner["id"]}] layout mosaic scroll {delta}');time.sleep(.6)
snap,ws,owner,after,scene=owner_state(name,proc,name+'-applied')
validate_camera(current,ws['mosaic']['rows'][0]['scroll_x'],delta,scene)
assert scene['clip_valid'] and scene['global_clip']==[-800,0,800,600]
assert not scene_from_log(log('compositor'),'HEADLESS-2')['clip_valid']
refstate=validate_reference(snap,refid,ref.pid)
camera_rows.append(dict(chain=name,before=current,delta=delta,after=scene['scroll'],before_owner=before,after_owner=after,scene=scene,reference=refstate))
save(lab,'camera-calibration',camera_rows)
if name=='E1':
stage='reference';inject('move',[-790,590]);time.sleep(.5)
first=capture('H2-reference-1','HEADLESS-2');time.sleep(.6)
second=capture('H2-reference-2','HEADLESS-2');cmp=reference(first,second)
save(lab,'reference-stability',dict(status='PASS',comparison=cmp,reference=refstate,interval='>=600ms',focus=snap['focused']))
global baseline
baseline=first
root_boundary[name]=time.monotonic_ns()
stage=name+'-open-A';topim=capture(name+'-top','HEADLESS-1')
topbox=paint(topim,'TOPLEVEL')['bbox'];assert topbox
# Tiled scene+window offset is checked against actual painted blue origin.
applied=applied_model(after,owner,log(name),name+'-mosaic')
content_rect=content(applied);origin=[content_rect.x,content_rect.y]
out=output_model(snap,'HEADLESS-1',content_rect.provenance)
verify_paint(content_rect,out,topbox,paint(topim,'TOPLEVEL')['count'],viewport_model(scene,content_rect.provenance))
assert topbox[0]-800==origin[0]
assert origin[1]==after['scene'][1]+owner['deco_rect']['height']+owner['window_rect']['y']
owners[name]=dict(id=owner['id'],pid=proc.pid,workspace=ws['id'],logical_rect=owner['rect'],applied=after,drawn_size=[420,320],paint=paint(topim,'TOPLEVEL'),content_origin=origin)
save(lab,'applied-owner-geometry',owners)
top_point=point(topim,'TOPLEVEL',-800)
require(0 <= top_point[0]-origin[0] < applied.native.rectangle.width and 0 <= top_point[1]-origin[1] < applied.native.rectangle.height, 'opening-point-native-input-bounds')
cp=click(name+'-open-A',name,top_point,True,'left')
wait(lambda:'POPUP_A MAP ' in log(name));time.sleep(.25)
correlate_pointer(name,top_point,content_rect.values(),'TOPLEVEL')
aim=capture(name+'-A','HEADLESS-1');ap=point(aim,'POPUP_A',-800)
stage=name+'-open-B';click(name+'-open-B',name,ap,True,'left')
wait(lambda:'POPUP_B MAP ' in log(name));time.sleep(.3)
prot=protocol(log(name));g=geometry(log(name),origin,content_rect.provenance)
# Actual configure/ACK/map drives geometry; requests are predictions only.
g['positioner_prediction']={'flags':0,'A':[100,80,350,170],'B':[100,60,300,130],'evidence':'source-backed prediction only'}
require(all(value=='EXERCISED' for value in g['crossing'].values()),'popup crossing NOT EXERCISED')
correlate_pointer(name,ap,g['A'],'POPUP_A')
left=capture(name+'-mosaic-H1','HEADLESS-1');right=capture(name+'-mosaic-H2','HEADLESS-2')
rgb=popup_pixels(left,right,g,True,baseline)
clip=root_clip(log('compositor'),origin,True,owner['id'],root_boundary[name],time.monotonic_ns())
chains[name]=dict(protocol=prot,geometry=g,pixels=rgb,owner=owners[name])
clips[name]=dict(tile=scene,root=clip,child=clip['child'])
save(lab,'grab-serials',{n:v['protocol']['grabs'] for n,v in chains.items()})
save(lab,'xdg-protocol-order',{n:v['protocol'] for n,v in chains.items()})
save(lab,'popup-root-geometry',{n:v['geometry']['A'] for n,v in chains.items()})
save(lab,'popup-nested-geometry',{n:v['geometry']['B'] for n,v in chains.items()})
save(lab,'applied-clips',clips);save(lab,'mosaic-pixels',{n:v['pixels'] for n,v in chains.items()})
return proc,owner,g,left
try:
comp=spawn('compositor',[lab/'swayfx-mosaic','-d','-c',run/'config'])
sock=wait(lambda:next(iter(runtime.glob('sway-ipc.*.sock')),None))
display=wait(lambda:next((x for x in runtime.glob('wayland-*') if x.is_socket()),None))
env.update(WAYLAND_DISPLAY=display.name,SWAYSOCK=str(sock))
assert Path(f'/proc/{comp.pid}/exe').resolve()==lab/'swayfx-mosaic'
maps=Path(f'/proc/{comp.pid}/maps').read_text();(run/'proc-maps.txt').write_text(maps)
paths=sorted({s.split()[-1] for s in maps.splitlines() if len(s.split())>=6 and s.split()[-1].startswith('/')})
wl=Path('/usr/lib/libwlroots-0.20.so').resolve()
assert [Path(x).resolve() for x in paths if 'libwlroots' in x]==[wl] and sha(wl)==WLROOTS_SHA
assert not any('libscenefx' in x for x in paths)
save(lab,'dependency-mappings',dict(status='PASS',paths=paths,wlroots=str(wl),wlroots_sha256=sha(wl),SceneFX_shared=False))
outputs=ipc('-t','get_outputs');validate_outputs(outputs);save(lab,'output-geometry',outputs)
pointer=spawn('pointer',[lab/'pointer-daemon']);wait(lambda:'POINTER_READY' in log('pointer'))
cmd('workspace 2');ref=spawn('reference',[lab/'static-reference'],debug=True)
rn=wait(lambda:find('org.mosaic.StaticReference',ref.pid));refid=rn['id'];cmd(f'[con_id={refid}] border none')
cmd('workspace 1');filler=spawn('filler',[lab/'static-reference'],debug=True)
wait(lambda:find('org.mosaic.StaticReference',filler.pid));cmd('layout mosaic')
E1,owner1,g1,im1=open_chain('E1')
stage='E1-visible-B';xy=point(im1,'POPUP_B',-800);row=click(stage,'E1',xy)
result=delivery(row,'E1','POPUP_B');coords=correlate_pointer('E1',xy,g1['B'],'POPUP_B');mapped(log('E1'))
save(lab,'mosaic-input',dict(status='PASS',pair=result,coordinates=coords,click=row))
stage='E1-forbidden-B';B=g1['B'];xy=[int((max(0,B[0])+min(800,B[0]+B[2]))//2),B[1]+30]
assert B[0]<=xy[0]<B[0]+B[2] and 8<=xy[0]<792
cut=len(log('E1'));row=click(stage,'E1',xy);time.sleep(.3)
ds=dismissal(log('E1')[cut:],row['events']['E1']);save(lab,'dismissal',ds)
refpair=row['events']['reference'];assert len(refpair) in [0,2]
save(lab,'forbidden-input',dict(status='PASS',click=row,popup_events=row['events']['E1'],reference_events=refpair,dismissal=ds))
inject('move',[-790,590]);clean=capture('E1-dismissed-H2','HEADLESS-2')
assert equal(baseline,clean)['equal'],'E1 dismissal residue'
close_client(E1,'E1','close_owner')
E2,owner2,g2,im2=open_chain('E2');assert owner2['id']!=owner1['id'] and E2.pid!=E1.pid
s1=[g['serial'] for g in chains['E1']['protocol']['grabs']];s2=[g['serial'] for g in chains['E2']['protocol']['grabs']]
assert len(set(s1+s2))==4 and max(s1)<min(s2),'serial reuse across chains'
stage='E2-standard';mapped(log('E2'));standard_boundary=time.monotonic_ns();reserve(lab,'transition');cmd(f'[con_id={owner2["id"]}] layout splith');time.sleep(.6)
snap,ws,std_owner,std_measure,std_scene=owner_state('E2',E2,'standard')
assert ws['id']==owners['E2']['workspace'] and ws['layout']=='splith'
if std_scene['clip_valid'] or std_scene['layout_enum']!=1:raise Defect('standard tiled clip retained')
mapped(log('E2'))
stdleft=capture('standard-H1','HEADLESS-1');stdright=capture('standard-H2','HEADLESS-2')
blue=paint(stdleft,'TOPLEVEL')['bbox'];assert blue
stdapplied=applied_model(std_measure,std_owner,log('E2'),'E2-standard')
stdcontent=content(stdapplied);stdorigin=[stdcontent.x,stdcontent.y]
fresh_standard(applied_model(owners['E2']['applied'],owners['E2']['applied']['IPC'],log('E2'),'E2-mosaic').scene,stdapplied.scene)
# Blue is occluded by A/B; full pixel mask checked against actual geometry below.
assert blue[0]-800==stdorigin[0] and blue[1]==stdorigin[1]
stdg=geometry(log('E2'),stdorigin,stdcontent.provenance);stdclip=root_clip(log('compositor'),stdorigin,False,owner2['id'],standard_boundary,time.monotonic_ns())
stdrgb=popup_pixels(stdleft,stdright,stdg,False,baseline)
save(lab,'standard-return',dict(status='PASS',same_workspace=ws['id'],owner=std_owner,applied=std_measure,scene=std_scene,root_clip=stdclip,child_clip='no independent clip in exact source; standard B pixels/input exercise removed inherited boundary',geometry=stdg,mapped_before_and_after=True,no_prior_popup_done=True))
verify_owner_occlusion(stdleft,stdright,stdcontent,stdg,False)
save(lab,'standard-popup-pixels',stdrgb)
stage='E2-standard-B';xy=point(stdright,'POPUP_B',0);row=click(stage,'E2',xy)
Bpair=delivery(row,'E2','POPUP_B');Bcoords=correlate_pointer('E2',xy,stdg['B'],'POPUP_B');mapped(log('E2'))
E2.stdin.write('close_b\n');E2.stdin.flush();wait(lambda:'COMMAND close_b DONE' in log('E2'))
assert 'POPUP_B DESTROY ' in log('E2') and 'POPUP_A DESTROY ' not in log('E2') and 'POPUP_A POPUP_DONE ' not in log('E2')
stage='E2-standard-A';Aimage=capture('standard-A-H2','HEADLESS-2');assert paint(Aimage,'POPUP_B')['count']==0
xy=point(Aimage,'POPUP_A',0);rowA=click(stage,'E2',xy);Apair=delivery(rowA,'E2','POPUP_A')
Acoords=correlate_pointer('E2',xy,stdg['A'],'POPUP_A')
save(lab,'standard-popup-input',dict(status='PASS',B=Bpair,A=Apair,B_coordinates=Bcoords,A_coordinates=Acoords,explicit_B_close=True,A_survived=True))
stage='E2-cleanup';close_client(E2,'E2','close_owner');time.sleep(.35)
final=capture('final-H2','HEADLESS-2');assert equal(baseline,final)['equal'],'final H2 residue'
assert not any(paint(final,n)['count'] for n in ['POPUP_A','POPUP_B'])
snap=snapshot('final');validate_reference(snap,refid,ref.pid)
assert filler.poll() is None and ref.poll() is None
measures=True;event('measurements-completed',status='PASS');stage='completed'
except Exception as exc:
failure=dict(type=type(exc).__name__,message=str(exc),stage=stage,verdict='BLOCKED' if isinstance(exc,Defect) else 'INCONCLUSIVE')
event('failure',**failure)
finally:
# WHY: shutdown transport outcome is not folded into check=True scientific gates.
exit_data=None
if comp is not None and comp.poll() is None and 'sock' in globals() and sock.is_socket():
# WHY: record transport evidence before wait can raise or time out.
def record_terminal(stdout,stderr):
(run/'terminal-exit.stdout').write_text(stdout)
(run/'terminal-exit.stderr').write_text(stderr)
exit_data=terminal_exchange(subprocess.run,comp.wait,
['swaymsg','-s',str(sock),'exit'],env,measures,
lambda:log('compositor'),
lambda:any(re.search(r'wl_display[^\n]*\.error\(|protocol error',log(n),re.I)
for n,_ in processes if n not in ['compositor','pointer']),
expired.is_set,record_terminal)
if exit_data is None:exit_data=dict(scientific_cleanup_pass=False,compositor_exit=comp.poll() if comp else None,measurements_completed=measures)
codes=[]
for name,proc in reversed(processes):
if proc.poll() is None:
try:proc.wait(timeout=.7)
except subprocess.TimeoutExpired:
if name=='pointer':proc.stdin.close() # normal EOF destroys virtual pointer
else:
rescue=True
try:os.killpg(proc.pid,signal.SIGTERM)
except ProcessLookupError:pass
try:proc.wait(timeout=.7)
except subprocess.TimeoutExpired:
rescue=True
try:os.killpg(proc.pid,signal.SIGKILL)
except ProcessLookupError:pass
proc.wait(timeout=.7)
codes.append(dict(name=name,pid=proc.pid,exit=proc.returncode))
if proc.stdin and not proc.stdin.closed:proc.stdin.close()
finished.set();thread.join(timeout=1)
for out in files:out.close()
for name,proc in processes:
try:os.killpg(proc.pid,0)
except ProcessLookupError:pass
else:rescue=True;os.killpg(proc.pid,signal.SIGKILL)
assert all(not Path('/proc',str(row['pid'])).exists() for row in codes),'owned process residual'
private_sockets=[str(p) for p in runtime.iterdir() if p.is_socket()]
shutil.rmtree(runtime)
exit_data.update(rescue_cleanup=rescue,owned_process_codes=codes)
exit_data['scientific_cleanup_pass']=bool(exit_data['scientific_cleanup_pass'] and not rescue and all(row['exit']==0 for row in codes))
exit_data['all_owned_reaped']=all(not Path('/proc',str(row['pid'])).exists() for row in codes)
if rescue:exit_data['scientific_cleanup_pass']=False
if measures and (not exit_data['scientific_cleanup_pass'] or any(r['exit']!=0 for r in codes)):
failure=dict(type='TerminalCleanupFailure',message='terminal/process evidence failed',stage='completed',verdict='INCONCLUSIVE')
save(lab,'terminal-exit',exit_data)
save(lab,'cleanup',dict(status='PASS' if not rescue else 'RESCUE',runtime=str(runtime),runtime_removed=not runtime.exists(),owned_processes=codes,sockets_before_owned_directory_removal=private_sockets,private_socket_residual=False))
save(lab,'runtime',dict(status='PASS' if failure is None else failure['verdict'],failure=failure,stage=stage,measurements_completed=measures,duration_seconds=time.monotonic()-started,watchdog=expired.is_set(),rescue_cleanup=rescue,runner_exit=0 if failure is None else 1))
verify(lab/'results/fixture-freeze-sha256.txt')
print('RUNTIME', 'PASS' if failure is None else failure)
raise SystemExit(0 if failure is None else 1)

View file

@ -0,0 +1,70 @@
"""Private probe ownership, durable budgets and bounded argv execution.
WHY: an exhausted experiment must not be restarted by replacing its LAB.
CONTRACT: stable exclusive owner and lock files; fsync precedes every action.
INVARIANT: failures consume all reservations, never refund or reset counters.
"""
import fcntl
import hashlib
import json
import os
from pathlib import Path
import subprocess
import tempfile
import time
REPO = Path(__file__).resolve().parents[3]
# No immutable compositor is built/copied and no runtime budget is initialized.
def sha(path):
return hashlib.sha256(Path(path).read_bytes()).hexdigest()
def save(lab, name, data):
(Path(lab)/'results'/(name+'.json')).write_text(json.dumps(data,indent=2)+'\n')
def durable(path, data):
fd,tmp=tempfile.mkstemp(prefix='.ledger-',dir=path.parent)
with os.fdopen(fd,'w') as out:
json.dump(data,out,indent=2);out.write('\n');out.flush();os.fsync(out.fileno())
os.replace(tmp,path)
fd=os.open(path.parent,os.O_RDONLY|os.O_DIRECTORY)
try:os.fsync(fd)
finally:os.close(fd)
def reserve(lab, *kinds):
from ledger import reserve as debit
return debit(Path(lab)/'results/budget.json', *kinds)
def environment():
# WHY: inherited desktop/loader settings must not select a daily socket.
excluded={'DISPLAY','WAYLAND_DISPLAY','SWAYSOCK','I3SOCK','XDG_RUNTIME_DIR',
'WAYLAND_DEBUG','DBUS_SESSION_BUS_ADDRESS','XDG_SESSION_ID','XDG_SEAT',
'XDG_VTNR','XDG_SESSION_TYPE','XDG_CURRENT_DESKTOP','XDG_SESSION_DESKTOP',
'LD_LIBRARY_PATH','LD_PRELOAD','LD_AUDIT','PKG_CONFIG_PATH','WLR_BACKENDS',
'WLR_RENDERER','WLR_HEADLESS_OUTPUTS','WLR_DRM_DEVICES','WLR_LIBINPUT_NO_DEVICES'}
env={k:v for k,v in os.environ.items() if k not in excluded and not k.startswith('WLR_')}
env.update(LC_ALL='C',PYTHONDONTWRITEBYTECODE='1')
return env
def command(lab,label,argv,cwd=None):
result=subprocess.run(list(map(str,argv)),cwd=cwd,env=environment(),capture_output=True,text=True,timeout=30)
(lab/'raw'/(label+'.stdout')).write_text(result.stdout)
(lab/'raw'/(label+'.stderr')).write_text(result.stderr)
with (lab/'raw/commands.jsonl').open('a') as out:
out.write(json.dumps(dict(label=label,argv=list(map(str,argv)),exit=result.returncode,cwd=str(cwd)))+'\n')
assert result.returncode==0,(label,result.returncode,result.stderr)
return result.stdout
def verify(manifest):
seen=set()
for row in Path(manifest).read_text().splitlines():
digest,p=row.split(' ',1)
assert p not in seen and sha(p)==digest,(manifest,p)
seen.add(p)
assert seen
return dict(entries=len(seen),sha256=sha(manifest))
def inventory(path, files):
with Path(path).open('x') as out:
for p in sorted(files):out.write(f'{sha(p)} {p}\n')
return verify(path)

View file

@ -0,0 +1,599 @@
#!/usr/bin/env python3
"""Synthetic negative branches and real historical replay; never launch clients."""
import argparse
from dataclasses import replace
import json
from pathlib import Path
import tempfile
import threading
import unittest
import sys
import re
from PIL import Image
import model as m
from model import *
from predicates import geometry,protocol,dismissal,terminal,root_clip,Defect,popup_pixels,COLORS,point,pair,mapped
from ledger import initial_for_offline_test,reserve,valid,LIMITS
from authorization import authorize,THIS_TICKET,MARKER
from replay import replay_native,replay_nested,color_geometry,HISTORICAL,NESTED
from support import save
HERE=Path(__file__).resolve().parent
RECEIPTS=[]
ACTIVE=None
TRACKED={str(p.resolve()) for p in HERE.glob('*.py')}
LINES={}
CONTRACTS={}
FAILED={}
def trace(frame,event,arg):
if ACTIVE and event=='line' and frame.f_code.co_filename in TRACKED:
key=frame.f_code.co_filename+':'+str(frame.f_lineno)
LINES.setdefault(ACTIVE,set()).add(key)
if ACTIVE and event=='exception' and arg[0] in (AssertionError,Invalid,Defect):
FAILED.setdefault(ACTIVE,set()).add(frame.f_code.co_filename+':'+str(frame.f_lineno))
if ACTIVE and event=='return' and frame.f_code.co_name=='require':
contract=frame.f_locals.get('contract');value=frame.f_locals.get('value')
CONTRACTS.setdefault(ACTIVE,set()).add((contract,bool(value)))
# CONTRACT: a rejected aggregation gate is an observed false predicate,
# not a raised exception and not a new graphical/scientific measurement.
if ACTIVE and event=='return' and frame.f_code.co_name=='need' and frame.f_code.co_filename==str(HERE/'write_results.py'):
ok=bool(frame.f_locals.get('ok'));name=frame.f_locals.get('name')
CONTRACTS.setdefault(ACTIVE,set()).add(('aggregate/'+str(name),ok))
if not ok and frame.f_back:
FAILED.setdefault(ACTIVE,set()).add(frame.f_back.f_code.co_filename+':'+str(frame.f_back.f_lineno))
return trace
class Case(unittest.TestCase):
def setUp(self):
global ACTIVE
ACTIVE=self.id();self.p=Provenance(9,6,'applied-1','synthetic applied trace')
self.a=Applied(Rect(Space.GLOBAL,-320,0,640,600,self.p),Rect(Space.CONTENT,2,0,636,573,self.p),Rect(Space.CONFIGURE,0,0,636,573,self.p),Native(Rect(Space.NATIVE,0,0,420,320,self.p),12,1680,1,20),2,25,25,21)
self.r=content(self.a);self.o=Output('H1',Rect(Space.GLOBAL,-800,0,800,600,self.p),1.0,'normal');self.clip=Rect(Space.VIEWPORT,-800,0,800,600,self.p)
def tearDown(self):
global ACTIVE
ACTIVE=None
def reject(self,contract,fn):
with self.assertRaisesRegex(Invalid,'^'+re.escape(contract)+'$'):fn()
def test_positive_geometry(self):
self.assertEqual(self.r.values(),[-318,25,636,573]);self.assertEqual(to_png(intersect(self.r,self.clip),self.o).values(),[482,25,318,573])
self.assertEqual(from_png(Rect(Space.PNG,482,25,318,573,self.p),self.o).values(),[-318,25,318,573])
verify_paint(self.r,self.o,[482,25,800,598],182214,self.clip)
def test_negative_native_height(self):self.reject('paint-origin-intersection',lambda:verify_paint(replace(self.r,height=320),self.o,[482,25,800,598],182214,self.clip))
def test_negative_scene_window_y(self):self.reject('paint-origin-intersection',lambda:verify_paint(replace(self.r,y=0),self.o,[482,25,800,598],182214,self.clip))
def test_negative_titlebar(self):self.reject('titlebar-content-offset',lambda:content(replace(self.a,titlebar=0)))
def test_negative_output_origin(self):self.reject('paint-origin-intersection',lambda:verify_paint(self.r,replace(self.o,rectangle=replace(self.o.rectangle,x=0)),[482,25,800,598],182214,self.clip))
def test_negative_png_space(self):self.reject('global-to-png-spaces',lambda:to_png(replace(self.r,space=Space.PNG),self.o))
def test_negative_png_bounds(self):self.reject('png-bounds',lambda:from_png(Rect(Space.PNG,-1,25,318,573,self.p),self.o))
def test_negative_assignment(self):self.reject('configure-assignment',lambda:content(replace(self.a,configured=replace(self.a.configured,width=420))))
def test_negative_workspace(self):self.reject('workspace-identity',lambda:content(replace(self.a,window=replace(self.a.window,provenance=replace(self.p,workspace=7)))))
def test_negative_owner(self):self.reject('owner-identity',lambda:content(replace(self.a,window=replace(self.a.window,provenance=replace(self.p,owner=10)))))
def test_negative_old_camera(self):self.reject('applied-generation',lambda:intersect(self.r,replace(self.clip,provenance=replace(self.p,generation='old-camera'))))
def test_negative_local_global_clip(self):self.reject('global-intersection',lambda:intersect(self.r,replace(self.clip,space=Space.CONTENT)))
def test_negative_buffer_identity(self):self.reject('native-buffer-identity',lambda:content(replace(self.a,native=replace(self.a.native,buffer_id=0))))
def test_negative_pending(self):self.reject('pending-not-applied',lambda:content(replace(self.a,scene=replace(self.a.scene,provenance=replace(self.p,state='pending')))))
def test_negative_scale(self):self.reject('unmeasured-output-scale',lambda:to_png(self.r,replace(self.o,scale=2.0)))
def test_negative_transform(self):self.reject('unmeasured-output-transform',lambda:to_png(self.r,replace(self.o,transform='90')))
def test_positive_popup(self):
A=popup(self.r,Rect(Space.POPUP,100,80,350,170,self.p),9,9,22,True)
B=popup(A,Rect(Space.POPUP,100,60,300,130,self.p),12,12,23,True)
self.assertEqual(A.values(),[-218,105,350,170]);self.assertEqual(B.values(),[-118,165,300,130]);self.assertEqual(crossing(B,0),'EXERCISED')
self.assertEqual(crossing(replace(B,x=1),0),'NOT EXERCISED')
pointer_local((-100,175),B,(18,10));constraints(0,[100,80,350,170],[100,80,350,170])
self.assertEqual(local_clip_to_global(Rect(Space.CONTENT,-482,-25,800,600,self.p),(-318,25),self.p).values(),[-800,0,800,600])
def test_negative_parent(self):self.reject('xdg-parent',lambda:popup(self.r,Rect(Space.POPUP,100,80,350,170,self.p),11,9,22,True))
def test_negative_ack(self):self.reject('popup-ack',lambda:popup(self.r,Rect(Space.POPUP,100,80,350,170,self.p),9,9,0,True))
def test_negative_map(self):self.reject('popup-map',lambda:popup(self.r,Rect(Space.POPUP,100,80,350,170,self.p),9,9,22,False))
def test_negative_constraints(self):self.reject('zero-flags-no-adjustment',lambda:constraints(0,[100,80,350,170],[99,80,350,170]))
def test_negative_pointer(self):self.reject('pointer-local-correlation',lambda:pointer_local((-308,35),self.r,(0,0)))
def test_negative_occlusion(self):
im=Image.new('RGB',(800,600));r=Rect(Space.GLOBAL,-800,0,1,1,self.p)
self.reject('replay-paint-POPUP_A',lambda:color_geometry(im,'POPUP_A',r,self.o,None))
def test_negative_standard_stale_origin(self):self.reject('fresh-standard-generation',lambda:fresh_standard(self.r,self.r))
def test_positive_standard_fresh(self):self.assertEqual(fresh_standard(self.r,replace(self.r,x=-398,provenance=replace(self.p,generation='standard-2'))).x,-398)
def test_negative_E2_identity(self):self.reject('fresh-E2-identity',lambda:fresh_chain(dict(owner=9,pid=10,serials=[1,2]),dict(owner=9,pid=11,serials=[3,4])))
def test_negative_E2_serials(self):self.reject('fresh-E2-serials',lambda:fresh_chain(dict(owner=9,pid=10,serials=[1,2]),dict(owner=10,pid=11,serials=[2,3])))
def test_positive_E2(self):fresh_chain(dict(owner=9,pid=10,serials=[1,2]),dict(owner=10,pid=11,serials=[3,4]))
def test_positive_terminal(self):
for ipc in (0,1):self.assertTrue(terminal(True,ipc,0,"Handling command 'exit'\nShutting down sway",False,False,stdout='actual reply',stderr='actual stderr')['scientific_cleanup_pass'])
def test_negative_terminal_incomplete(self):self.assertFalse(terminal(False,1,0,"Handling command 'exit'\nShutting down sway",False,False)['scientific_cleanup_pass'])
def test_negative_terminal_unhandled(self):self.assertFalse(terminal(True,1,0,'Shutting down sway',False,False)['scientific_cleanup_pass'])
def test_negative_terminal_compositor(self):self.assertFalse(terminal(True,1,1,"Handling command 'exit'\nShutting down sway",False,False)['scientific_cleanup_pass'])
def test_negative_terminal_protocol(self):self.assertFalse(terminal(True,1,0,"Handling command 'exit'\nShutting down sway",True,False)['scientific_cleanup_pass'])
def test_negative_terminal_rescue(self):self.assertFalse(terminal(True,1,0,"Handling command 'exit'\nShutting down sway",False,True)['scientific_cleanup_pass'])
def test_negative_dismissal_hit(self):
with self.assertRaisesRegex(Defect,'invisible popup'):dismissal('POPUP_B POPUP_DONE \nPOPUP_A POPUP_DONE \nPOPUP_B DESTROY \nPOPUP_A DESTROY ',['POINTER_BUTTON target=POPUP_B serial=22 button=273 state=1'])
def test_negative_dismissal_incomplete(self):
with self.assertRaises(AssertionError):dismissal('POPUP_A POPUP_DONE ',[])
def test_positive_dismissal(self):self.assertEqual(dismissal('POPUP_B POPUP_DONE \nPOPUP_A POPUP_DONE \nPOPUP_B DESTROY \nPOPUP_A DESTROY ',[])['status'],'PASS')
def test_positive_button(self):pair(['POINTER_BUTTON target=POPUP_B serial=22 button=273 state=1','POINTER_BUTTON target=POPUP_B serial=23 button=273 state=0'],'POPUP_B')
def test_negative_button(self):
with self.assertRaises(Defect):pair(['POINTER_BUTTON target=POPUP_A serial=22 button=273 state=1'],'POPUP_B')
def test_negative_root_ambiguous(self):
trace='PI_OWNER output=HEADLESS-1 ns=10 id=9 scene_valid=1\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=1 clip_valid=1 clip=-482,-25,800,600\nPI_POPUP output=HEADLESS-1 ns=12 local_index=2 tree=0x2 enabled=1 clip_valid=1 clip=-482,-25,800,600'
self.reject('root-chain-unique',lambda:root_clip(trace,[-318,25],True,9,1,20))
def test_positive_root(self):
trace='PI_OWNER output=HEADLESS-1 ns=10 id=9 scene_valid=1\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=1 clip_valid=1 clip=-482,-25,800,600'
self.assertTrue(root_clip(trace,[-318,25],True,9,1,20)['clip_valid'])
def test_negative_future_gate(self):self.reject('explicit-future-authorization-required',lambda:authorize('/does/not/exist',None))
def test_negative_current_ticket_gate(self):
with tempfile.TemporaryDirectory(prefix='geometry-auth-test-') as tmp:
f=Path(tmp)/'auth.json';f.write_text(json.dumps(dict(scope='one-new-static-nested-headless-run',explicit_user_authorization=True,ticket=THIS_TICKET)))
self.reject('distinct-future-ticket-required',lambda:authorize(tmp,f))
def test_real_native_replay(self):replay_native(LAB)
def test_real_nested_replay(self):
rows=replay_nested(LAB)
crossing=next(r for r in rows if r['case']=='run-private_mosaic-crossing-b_cross')
self.assertEqual(crossing['B'][:2],[662,165])
standard=next(r for r in rows if r['case']=='run-private_mosaic-toggle-b_cross')
sample=next(c for c in standard['input_correlation']['callbacks'] if c['target']=='POPUP_B')
self.assertEqual(sample['origin'],[622,165]);self.assertEqual(sample['global_point'],[900,190]);self.assertEqual(sample['local'],[278,25])
def test_positive_protocol(self):protocol(self.protocol_text())
def protocol_text(self):
text=(NESTED/'run-private_mosaic-crossing-b_cross/client.log').read_text();return text[:text.index('POPUP_B POPUP_DONE ')]
def test_negative_protocol_serial(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('serial=55 used=55','serial=0 used=0'))
def test_negative_protocol_missing_serial(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('POPUP_A GRAB_REQUEST','MISSING GRAB_REQUEST'))
def test_negative_protocol_parent(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('parent=POPUP_A parent_xdg=12','parent=TOPLEVEL parent_xdg=9'))
def test_negative_protocol_ACK(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('xdg_surface#12.ack_configure(56)','xdg_surface#12.ack_configure(0)'))
def test_negative_protocol_map(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('POPUP_B MAP ','POPUP_B NOTMAP '))
def test_negative_protocol_reused_objects(self):
with self.assertRaises(AssertionError):protocol(self.protocol_text().replace('POPUP_B CREATE wl=13','POPUP_B CREATE wl=11'))
def test_positive_ledger_exhaustion(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);reserve(p,'run');before=p.read_bytes()
self.reject('ledger-exhausted',lambda:reserve(p,'run'));self.assertEqual(p.read_bytes(),before)
with self.assertRaises(FileExistsError):initial_for_offline_test(p)
def test_negative_ledger_corruption(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);s=json.loads(p.read_text());s['used']['run']=True;p.write_text(json.dumps(s))
self.reject('ledger-counts',lambda:reserve(p,'run'))
s['used']['run']=1;p.write_text(json.dumps(s));self.reject('ledger-events',lambda:reserve(p,'run'))
def test_positive_ledger_concurrency(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);wins=[];fails=[]
def debit():
try:reserve(p,'run');wins.append(1)
except Invalid:fails.append(1)
ts=[threading.Thread(target=debit) for _ in range(8)]
for t in ts:t.start()
for t in ts:t.join()
self.assertEqual((len(wins),len(fails)),(1,7));valid(json.loads(p.read_text()))
def test_negative_ledger_partial_bundle(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);reserve(p,'run');before=p.read_bytes()
self.reject('ledger-exhausted',lambda:reserve(p,'click','run'));self.assertEqual(before,p.read_bytes())
def test_negative_ledger_unknown(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);self.reject('ledger-debit-kinds',lambda:reserve(p,'reset'))
def test_negative_ledger_missing(self):self.reject('existing-ledger-required',lambda:reserve('/tmp/absent-geometry-ledger-never-created','run'))
def test_positive_empty_intersection(self):
r=replace(self.r,x=1000);verify_paint(r,self.o,None,0,self.clip)
self.assertEqual(to_png(r,self.o).width,0)
def popup_images(self,mosaic):
from PIL import ImageDraw
g={'A':[-20,10,40,40],'B':[-10,20,30,20],'provenance':dict(owner=9,workspace=6,generation='applied-1',evidence='synthetic mask',state='applied')}
ims=[]
for ox in (-800,0):
im=Image.new('RGB',(800,600),(48,48,56));draw=ImageDraw.Draw(im)
for key,name in [('A','POPUP_A'),('B','POPUP_B')]:
x,y,w,h=g[key];left=max(x,ox);right=min(x+w,ox+800)
if left<right and (not mosaic or ox==-800):draw.rectangle((left-ox,y,right-ox-1,y+h-1),fill=COLORS[name])
ims.append(im)
return g,*ims,Image.new('RGB',(800,600),(48,48,56))
def test_positive_popup_pixels(self):
for mosaic in (True,False):
g,left,right,base=self.popup_images(mosaic);popup_pixels(left,right,g,mosaic,base)
def test_negative_popup_pixels_forbidden(self):
g,left,right,base=self.popup_images(True);right.putpixel((1,21),COLORS['POPUP_B'])
self.reject('replay-paint-POPUP_B',lambda:popup_pixels(left,right,g,True,base))
def test_negative_popup_pixels_occlusion(self):
g,left,right,base=self.popup_images(True);left.putpixel((795,21),COLORS['POPUP_A'])
self.reject('replay-paint-POPUP_A',lambda:popup_pixels(left,right,g,True,base))
def test_negative_popup_pixels_reference(self):
g,left,right,base=self.popup_images(True);right.putpixel((300,300),(1,2,3))
with self.assertRaises(Defect):popup_pixels(left,right,g,True,base)
def test_negative_popup_pixels_provenance(self):
g,left,right,base=self.popup_images(True);g.pop('provenance');self.reject('popup-paint-provenance',lambda:popup_pixels(left,right,g,True,base))
def test_negative_popup_pixels_standard_absent(self):
g,left,right,base=self.popup_images(True)
self.reject('replay-paint-POPUP_A',lambda:popup_pixels(left,right,g,False,base))
def test_negative_output_image_dimensions(self):
self.reject('replay-output-size',lambda:color_geometry(Image.new('RGB',(799,600)),'TOPLEVEL',self.r,self.o,None))
def historical_applied_inputs(self):
from observations import applied_model
cal=json.loads((HISTORICAL/'results/camera-calibration.json').read_text())[-1]
measured={**cal['after_owner'],'workspace':cal['scene']['workspace']};return measured,measured['IPC'],(HISTORICAL/'run/E1.log').read_text()
def test_negative_native_natural_geometry(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();changed={**owner,'geometry':{**owner['geometry'],'x':1}}
measured['IPC']=changed;self.reject('native-natural-geometry',lambda:applied_model(measured,changed,text,'test'))
def test_positive_applied_adapter(self):
from observations import applied_model,output_model,viewport_model
measured,owner,text=self.historical_applied_inputs();a=applied_model(measured,owner,text,'historical-adapter');self.assertEqual(a.configure_ack,21)
snap=json.loads((HISTORICAL/'results/E1-applied-snapshot.json').read_text());output_model(snap,'HEADLESS-1',a.scene.provenance)
viewport_model({'workspace':6,'clip_valid':True,'global_clip':[-800,0,800,600]},a.scene.provenance)
def test_negative_applied_adapter_owner(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('measured-owner-identity',lambda:applied_model({**measured,'id':10},owner,text,'test'))
def test_negative_applied_adapter_workspace(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();measured.pop('workspace');self.reject('measured-workspace-required',lambda:applied_model(measured,owner,text,'test'))
def test_negative_native_trace_missing(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('native-shm-trace-required',lambda:applied_model(measured,owner,text.replace('create_buffer(','not_create_buffer['),'test'))
def test_negative_native_trace_after_map(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('toplevel-buffer-before-map',lambda:applied_model(measured,owner,'TOPLEVEL MAP early\n'+text,'test'))
def test_negative_native_attach(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('native-toplevel-attach',lambda:applied_model(measured,owner,text.replace('wl_surface#3.attach(wl_buffer#12','wl_surface#3.attach(wl_buffer#999'),'test'))
def test_negative_toplevel_configure_missing(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('toplevel-configure-required',lambda:applied_model(measured,owner,text.replace('TOPLEVEL ROLE_CONFIGURE w=636 h=573','TOPLEVEL ROLE_CONFIGURE w=0 h=0'),'test'))
def test_negative_assigned_ACK_trace(self):
from observations import applied_model
measured,owner,text=self.historical_applied_inputs();self.reject('assigned-ack-trace',lambda:applied_model(measured,owner,text.replace('xdg_surface#9.ack_configure(21)','xdg_surface#9.ack_configure(999)'),'test'))
def test_negative_output_unique(self):
from observations import output_model
self.reject('unique-active-output',lambda:output_model({'outputs':[]},'HEADLESS-1',self.p))
def test_negative_viewport_workspace(self):
from observations import viewport_model
self.reject('viewport-workspace',lambda:viewport_model({'workspace':7,'clip_valid':True,'global_clip':[-800,0,800,600]},self.p))
def test_negative_viewport_valid(self):
from observations import viewport_model
self.reject('viewport-applied-valid',lambda:viewport_model({'workspace':6,'clip_valid':False,'global_clip':[-800,0,800,600]},self.p))
def test_positive_client_preparation(self):
from prepare_clients import prepare
with tempfile.TemporaryDirectory(prefix='geometry-client-compile-test-') as tmp:
lab=Path(tmp);(lab/'raw').mkdir();(lab/'results').mkdir();prepare(lab)
def test_negative_client_source_identity(self):
import prepare_clients as pc
from unittest.mock import patch
import shutil
with tempfile.TemporaryDirectory(prefix='geometry-client-identity-test-') as tmp:
root=Path(tmp);(root/'raw').mkdir();(root/'results').mkdir();fake=root/'probes'
for dirname in ('step20c-nested-grab','step20c-valid-grab','step20c-saved-target-timeout-input','step20c-static-nested-grab'):(fake/dirname).mkdir(parents=True)
for rel in ('step20c-nested-grab/nested-client.c','step20c-valid-grab/pointer-daemon.c','step20c-saved-target-timeout-input/static-reference.c','step20c-saved-target-timeout-input/saved-client.c','step20c-static-nested-grab/placement.patch'):
shutil.copyfile(pc.PROBES/rel,fake/rel)
nested=fake/'step20c-nested-grab/nested-client.c';nested.write_text(nested.read_text()+'\n/* corrupted fixture identity */\n')
with patch.object(pc,'PROBES',fake):self.reject('frozen-nested-source',lambda:pc.prepare(root))
def test_negative_client_placement_identity(self):
import prepare_clients as pc
from unittest.mock import patch
import shutil
with tempfile.TemporaryDirectory(prefix='geometry-client-identity-test-') as tmp:
root=Path(tmp);(root/'raw').mkdir();(root/'results').mkdir();fake=root/'probes'
for dirname in ('step20c-nested-grab','step20c-valid-grab','step20c-saved-target-timeout-input','step20c-static-nested-grab'):(fake/dirname).mkdir(parents=True)
for rel in ('step20c-nested-grab/nested-client.c','step20c-valid-grab/pointer-daemon.c','step20c-saved-target-timeout-input/static-reference.c','step20c-saved-target-timeout-input/saved-client.c'):
shutil.copyfile(pc.PROBES/rel,fake/rel)
(fake/'step20c-static-nested-grab/placement.patch').write_text('corrupt recorded patch')
with patch.object(pc,'PROBES',fake):self.reject('byte-identical-placement',lambda:pc.prepare(root))
def altered_client_contract(self,field,contract):
import prepare_clients as pc
from unittest.mock import patch
import shutil
with tempfile.TemporaryDirectory(prefix='geometry-client-contract-test-') as tmp:
root=Path(tmp);(root/'raw').mkdir();(root/'results').mkdir();here=root/'fixture';here.mkdir();shutil.copyfile(pc.HERE/'placement.patch',here/'placement.patch')
data=json.loads((pc.HERE/'client-contract.json').read_text())
if field=='adapted':data['adapted_nested_sha256']='corrupt hash'
else:data['protocols'][field]='corrupt hash'
(here/'client-contract.json').write_text(json.dumps(data))
with patch.object(pc,'HERE',here):self.reject(contract,lambda:pc.prepare(root))
def test_negative_client_adapted_identity(self):self.altered_client_contract('adapted','byte-identical-adapted-client')
def test_negative_client_xdg_header(self):self.altered_client_contract('xdg-shell-client.h','byte-identical-protocol-xdg-shell-client.h')
def test_negative_client_xdg_code(self):self.altered_client_contract('xdg-shell-protocol.c','byte-identical-protocol-xdg-shell-protocol.c')
def test_negative_client_pointer_header(self):self.altered_client_contract('virtual-pointer-client.h','byte-identical-protocol-virtual-pointer-client.h')
def test_negative_client_pointer_code(self):self.altered_client_contract('virtual-pointer-protocol.c','byte-identical-protocol-virtual-pointer-protocol.c')
def test_positive_owner_occlusion(self):
from observations import verify_owner_occlusion
left=Image.new('RGB',(800,600));right=Image.new('RGB',(800,600));r=Rect(Space.GLOBAL,-800,0,1,1,self.p);left.putpixel((0,0),COLORS['TOPLEVEL'])
g={'A':[1000,0,1,1],'B':[1000,0,1,1]};verify_owner_occlusion(left,right,r,g,True)
left.putpixel((0,0),(0,0,0));self.reject('replay-paint-TOPLEVEL',lambda:verify_owner_occlusion(left,right,r,g,True))
def test_positive_inventory_checker(self):
self.make_register_check()
def make_register_check(self,corrupt=None,contract=None,proof=None):
from assertions import HERE,REPO,HISTORY,HISTORICAL_FILES,inventory,classify,check
from support import sha
with tempfile.TemporaryDirectory(prefix='geometry-register-test-') as tmp:
lab=Path(tmp);(lab/'results').mkdir()
paths=[HISTORY/n for n in HISTORICAL_FILES]+[HERE/'model.py']
records=[classify(r) for p in paths for r in inventory(p)]
for r in records:r.update(positive_executed_test_ids=[],negative_executed_test_ids=[],test_status='NOT TESTED runtime dependency')
register={'source_inventory':{str(p.relative_to(REPO)):sha(p) for p in paths},'records':records}
if corrupt:corrupt(register)
(lab/'results/assertion-register.json').write_text(json.dumps(register));(lab/'results/test-receipts.json').write_text(json.dumps({'tests':proof or []}))
if contract:self.reject(contract,lambda:check(lab))
else:self.assertEqual(check(lab)['historical_asserts'],145)
def test_negative_inventory_counterfeit_receipt(self):
self.make_register_check(lambda r:r['records'][0].update(positive_executed_test_ids=['already-passed-other-test']),'register-predicate-receipt-correlation',[{'id':'already-passed-other-test','status':'PASS','executed_lines':[]}])
def test_negative_inventory_missing(self):self.make_register_check(lambda r:r['records'].pop(),'register-exhaustive-unique')
def test_negative_inventory_duplicate(self):self.make_register_check(lambda r:r['records'].append(r['records'][0]),'register-exhaustive-unique')
def test_negative_inventory_stale_source(self):self.make_register_check(lambda r:r['source_inventory'].update({next(iter(r['source_inventory'])):'wrong'}),'register-source-freshness')
def test_negative_inventory_unclassified(self):self.make_register_check(lambda r:r['records'][0].update(domain=''),'register-classified')
def test_negative_inventory_stale_AST(self):self.make_register_check(lambda r:r['records'][0].update(canonical_hash='wrong'),'register-ast-freshness')
def test_negative_inventory_untested_claim(self):self.make_register_check(lambda r:r['records'][0].update(positive_executed_test_ids=['never executed']),'register-executed-receipts')
def test_positive_authorization_pure(self):
with tempfile.TemporaryDirectory(prefix='geometry-auth-test-') as tmp:
root=Path(tmp);(root/'results').mkdir()
auth=dict(scope='one-new-static-nested-headless-run',explicit_user_authorization=True,ticket='synthetic-future-unit-test',registered_lab=str(root),owner_registry='test-only-owner',binary='test-only-binary',binary_sha256='test-only-hash',wlroots_sha256='test-only-hash')
f=root/'auth.json';f.write_text(json.dumps(auth));(root/'results/offline-gate.json').write_text(json.dumps(dict(marker=MARKER)));(root/'results/independent-review.json').write_text(json.dumps(dict(status='ACCEPTED',independent=True)))
self.assertEqual(authorize(root,f),auth)
(root/'run').mkdir();self.reject('fresh-run-required',lambda:authorize(root,f));(root/'run').rmdir()
(root/'results/independent-review.json').write_text(json.dumps(dict(status='NOT TESTED',independent=True)))
self.reject('completed-offline-review-required',lambda:authorize(root,f))
(root/'results/independent-review.json').write_text(json.dumps(dict(status='ACCEPTED',independent=True)));auth.pop('binary');f.write_text(json.dumps(auth));self.reject('future-input-provenance',lambda:authorize(root,f))
auth['registered_lab']='wrong';f.write_text(json.dumps(auth));self.reject('registered-fresh-lab-required',lambda:authorize(root,f))
def test_negative_offline_lab_authorization(self):
with tempfile.TemporaryDirectory(prefix='geometry-auth-test-') as tmp:
root=Path(tmp);f=root/'auth.json';f.write_text(json.dumps(dict(scope='one-new-static-nested-headless-run',explicit_user_authorization=True,ticket='synthetic-future-unit-test',registered_lab=str(LAB.resolve()))))
self.reject('historical-or-offline-lab-forbidden',lambda:authorize(LAB,f))
def test_negative_ledger_sequences(self):
with tempfile.TemporaryDirectory(prefix='geometry-ledger-test-') as tmp:
p=Path(tmp)/'budget.json';initial_for_offline_test(p);reserve(p,'click');state=json.loads(p.read_text());state['events'][0]['seq']=5
self.reject('ledger-sequences',lambda:valid(state));state['events'][0]['seq']=0;state['events'][0]['kind']='run'
self.reject('ledger-accounting',lambda:valid(state));state['limits']['run']=2;self.reject('ledger-schema',lambda:valid(state))
def test_negative_ledger_test_scope(self):
with tempfile.TemporaryDirectory(prefix='geometry-other-test-') as tmp:self.reject('test-ledger-only',lambda:initial_for_offline_test(Path(tmp)/'budget.json'))
def test_positive_negative_geometry_shared_protocol(self):
g=geometry(self.protocol_text(),[-318,25],self.p)
self.assertEqual(g['A'],[-118,105,300,170]);self.assertEqual(g['B'],[102,165,300,130]);self.assertEqual(g['crossing']['B'],'NOT EXERCISED')
self.reject('popup-owner-provenance-required',lambda:geometry(self.protocol_text(),[-318,25]))
def test_negative_popup_native_attach(self):
text=self.protocol_text();text=re.sub(r'wl_surface#11.attach\(wl_buffer#\d+', 'wl_surface#11.attach(null',text)
self.reject('popup-native-attach',lambda:protocol(text))
def test_negative_popup_native_size(self):
text=self.protocol_text();text=text.replace(', 0, 300, 170, 1200, 1)',', 0, 299, 170, 1196, 1)')
self.reject('popup-native-configured-size',lambda:protocol(text))
def test_negative_debug_parent(self):
self.reject('debug-parent-request',lambda:protocol(self.protocol_text().replace('xdg_surface#12.get_popup','xdg_surface#999.get_popup')))
def test_negative_debug_button(self):
self.reject('debug-real-button-serial',lambda:protocol(self.protocol_text().replace('wl_pointer#8.button(55,','wl_pointer#8.button(999,')))
def test_negative_debug_popup_configure(self):
self.reject('debug-popup-configure',lambda:protocol(self.protocol_text().replace('xdg_popup#14.configure(200,','xdg_popup#14.configure(999,')))
def test_negative_debug_xdg_configure(self):
self.reject('debug-xdg-configure',lambda:protocol(self.protocol_text().replace('xdg_surface#12.configure(56)','xdg_surface#12.configure(999)')))
def test_negative_root_missing(self):self.reject('bounded-root-owner-observations',lambda:root_clip('',[-318,25],True,9,1,20))
def test_negative_root_format(self):self.reject('root-trace-format',lambda:root_clip('PI_OWNER output=HEADLESS-1 ns=10 id=9 x\nPI_POPUP output=HEADLESS-1 ns=11 bad',[-318,25],True,9,1,20))
def test_negative_root_state(self):
text='PI_OWNER output=HEADLESS-1 ns=10 id=9 x\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=1 clip_valid=0 clip=0,0,0,0'
with self.assertRaises(Defect):root_clip(text,[-318,25],True,9,1,20)
self.assertFalse(root_clip(text,[-318,25],False,9,1,20)['clip_valid'])
def test_negative_root_clip_origin(self):self.reject('root-applied-global-clip',lambda:root_clip('PI_OWNER output=HEADLESS-1 ns=10 id=9 x\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=1 clip_valid=1 clip=0,0,800,600',[-318,25],True,9,1,20))
def test_negative_root_unstable(self):
text='PI_OWNER output=HEADLESS-1 ns=10 id=9 x\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=1 clip_valid=0 clip=0,0,0,0\nPI_POPUP output=HEADLESS-1 ns=12 local_index=1 tree=0x1 enabled=1 clip_valid=1 clip=-482,-25,800,600'
self.reject('root-window-state-consistent',lambda:root_clip(text,[-318,25],True,9,1,20))
def test_negative_root_enabled(self):self.reject('root-enabled-index',lambda:root_clip('PI_OWNER output=HEADLESS-1 ns=10 id=9 x\nPI_POPUP output=HEADLESS-1 ns=11 local_index=1 tree=0x1 enabled=0 clip_valid=1 clip=-482,-25,800,600',[-318,25],True,9,1,20))
def correlation_fixture(self,name='run-private_mosaic-crossing-b_cross'):
from replay import correlate_historical
d=NESTED/name;tree=json.loads((d/'tree-open.json').read_text())
from ipc_predicates import nodes
owner=next(n for n in nodes(tree) if n.get('app_id')=='org.mosaic.NestedGrabProbe')
comp=(d/'compositor.log').read_text()
c=re.findall(r'PROBE_POPUP_CLIP owner=(\S+) local=(-?\d+),(-?\d+) (\d+)x(\d+)',comp)[0]
origin=(-int(c[1]),-int(c[2]));text=(d/'client.log').read_text()
rects={'TOPLEVEL':Rect(Space.GLOBAL,*origin,owner['window_rect']['width'],owner['window_rect']['height'],self.p)}
for target,parent in [('POPUP_A','TOPLEVEL'),('POPUP_B','POPUP_A')]:
x,y,w,h=map(int,re.findall(target+r' ROLE_CONFIGURE x=(-?\d+) y=(-?\d+) w=(\d+) h=(\d+)',text)[-1]);r=rects[parent]
rects[target]=Rect(Space.GLOBAL,r.x+x,r.y+y,w,h,self.p)
return correlate_historical,text,(d/'pointer.log').read_text(),rects
def test_positive_historical_wire_correlation(self):
fn,text,inject,rects=self.correlation_fixture();r=fn(text,inject,rects)
self.assertEqual(r['status'],'PASS');self.assertEqual(r['buttons'][4]['msec'],1008)
self.assertEqual(r['callbacks'][-1]['local'],[38,25])
def test_negative_historical_all_coordinates(self):
fn,text,inject,rects=self.correlation_fixture()
self.reject('historical-coordinate-wire-local',lambda:fn(re.sub(r'(POINTER_(?:ENTER|MOTION)[^\n]* x=)[\d.-]+',r'\g<1>99999.00',text),inject,rects))
def test_negative_historical_both_wire_callback_coordinates(self):
fn,text,inject,rects=self.correlation_fixture()
bad=text.replace('x=38.00 y=25.00','x=99999.00 y=25.00').replace('38.00000000, 25.00000000','99999.00000000, 25.00000000')
self.reject('pointer-local-correlation',lambda:fn(bad,inject,rects))
def test_negative_historical_debug_motion_coordinate(self):
fn,text,inject,rects=self.correlation_fixture('run-private_mosaic-close_b-visible')
self.reject('historical-coordinate-wire-local',lambda:fn(text.replace('motion(1003, 38.00000000','motion(1003, 99999.00000000'),inject,rects))
def test_negative_historical_recipient(self):
fn,text,inject,rects=self.correlation_fixture()
self.reject('historical-enter-surface-identity',lambda:fn(text.replace('POINTER_ENTER target=POPUP_B','POINTER_ENTER target=POPUP_A'),inject,rects))
def test_negative_historical_additional_invisible_button(self):
fn,text,inject,rects=self.correlation_fixture()
bad=text.replace('POPUP_B POPUP_DONE ','POINTER_BUTTON target=POPUP_B serial=999 button=273 state=1\nPOPUP_B POPUP_DONE ')
self.reject('historical-button-wire-present',lambda:fn(bad,inject,rects))
def test_negative_historical_button_order(self):
fn,text,inject,rects=self.correlation_fixture()
self.reject('historical-button-wire-identity',lambda:fn(text.replace('serial=65 button=273 state=1','serial=65 button=273 state=0'),inject,rects))
def test_positive_historical_map_retarget(self):
fn,text,inject,rects=self.correlation_fixture('run-private_mosaic-close_b-visible');r=fn(text,inject,rects)
enters=[c for c in r['callbacks'] if c['target']=='POPUP_A']
self.assertEqual(enters[0]['global_point'],[340,150]);self.assertEqual(enters[0]['local'],[48,45])
self.assertEqual(r['buttons'][-1]['phase'],'after-B-close')
def exchange(self,ipc=1,measures=True,timeout=False,invocation=False):
import subprocess
from types import SimpleNamespace
from predicates import terminal_exchange
def execute(*a,**k):
if invocation:raise OSError('synthetic invocation failure')
return SimpleNamespace(returncode=ipc,stdout='actual stdout',stderr='actual stderr')
def wait(**k):
if timeout:raise subprocess.TimeoutExpired('synthetic-compositor',3)
return 0
recorded=[]
data=terminal_exchange(execute,wait,['synthetic'],{},measures,
lambda:"Handling command 'exit'\nShutting down sway",lambda:False,lambda:False,
lambda out,err:recorded.append((out,err)))
return data,recorded
def test_positive_terminal_exchange_transport(self):
data,recorded=self.exchange();self.assertTrue(data['scientific_cleanup_pass'])
self.assertEqual(data['ipc_exit'],1);self.assertTrue(data['transport_incident'])
self.assertEqual(recorded,[('actual stdout','actual stderr')])
def test_negative_terminal_exchange_wait_timeout(self):
data,recorded=self.exchange(ipc=7,timeout=True)
self.assertEqual(data['ipc_exit'],7);self.assertEqual(data['stdout'],'actual stdout')
self.assertEqual(data['stderr'],'actual stderr');self.assertIn('compositor_error',data)
self.assertFalse(data['scientific_cleanup_pass']);self.assertEqual(len(recorded),1)
def test_negative_terminal_exchange_incomplete(self):
self.assertFalse(self.exchange(measures=False)[0]['scientific_cleanup_pass'])
def test_negative_terminal_exchange_invocation(self):
data,recorded=self.exchange(invocation=True);self.assertIsNone(data['ipc_exit'])
self.assertIn('ipc_error',data);self.assertFalse(data['scientific_cleanup_pass']);self.assertEqual(recorded,[])
def aggregate_fixture(self):
from write_results import REQUIRED,aggregate
from support import sha
evidence={n:json.loads((LAB/'results'/(n+'.json')).read_text()) for n in REQUIRED}
# CONTRACT: all acceptance here is a synthetic complete snapshot in memory.
# The real receipts are written only after the entire suite finishes.
evidence['test-receipts']['status']='PASS'
for receipt in evidence['test-receipts']['tests']:receipt['status']='PASS'
# CONTRACT: this is synthetic independent acceptance in memory only.
bindings={'source_delta':{'fixture':'synthetic-final-hash'},'evidence_sha256':{'proof':'synthetic-proof-hash'}}
evidence['independent-review']=dict(status='ACCEPTED',independent=True,**bindings)
# INVARIANT: immutable synthetic hash provider avoids bootstrapping current
# test receipts from the suite that is still producing those receipts.
# WHY: source inventories in this synthetic snapshot must describe the
# same bytes even while the real on-disk register awaits regeneration.
evidence['test-receipts']['source_inventory']={n:sha(n) for n in evidence['test-receipts']['source_inventory']}
evidence['assertion-register']['source_inventory']={n:sha(HERE.parents[2]/n) for n in evidence['assertion-register']['source_inventory']}
hashes={}
for name in ('historical-evidence','client-provenance','test-receipts'):
hashes.update(evidence[name].get('inputs',{}));hashes.update(evidence[name].get('source_inventory',{}))
reg=evidence['assertion-register'];hashes.update({str(HERE.parents[2]/n):v for n,v in reg['source_inventory'].items()});hashes.update(reg['artifact_inventory'])
audit=evidence['source-audit'];hashes.update({c['source']:c['sha256'] for c in audit['contracts']})
hashes[audit['source_version_receipt']]=audit['source_version_sha256']
for case in evidence['historical-replay']['cases']:
hashes.update({str(NESTED/case['case']/n):v for n,v in case['files'].items()})
client=evidence['client-provenance'];hashes[str(HERE/'placement.patch')]=client['patch']
builds={v['client']:v for v in client['builds']}
for command in client['commands']:
label=command['label'];argv=command['argv']
if label.endswith('-compile') and label[:-8] in builds:
build=builds[label[:-8]];source=next(v for v in argv if v.endswith('/'+label[:-8]+'.c'))
hashes[source]=build['source'];hashes[argv[argv.index('-o')+1]]=build['binary']
hashes.update({str(Path(source).parent/n):v for n,v in client['protocols'].items()})
return aggregate,evidence,lambda path:hashes.get(str(path)),bindings
def test_positive_aggregate_complete_bound(self):
fn,e,h,b=self.aggregate_fixture();result=fn(e,h,b)
self.assertEqual(result['status'],'READY_FOR_NEW_RUNTIME')
self.assertEqual(set(result['markers'].values()),{'PASS'})
def test_negative_aggregate_review_stale(self):
fn,e,h,b=self.aggregate_fixture();e['independent-review']['source_delta']={}
self.assertEqual(fn(e,h,b)['status'],'INCONCLUSIVE')
def test_negative_aggregate_review_unaccepted(self):
fn,e,h,b=self.aggregate_fixture();e['independent-review']['status']='CORRECTION_REQUIRED'
self.assertEqual(fn(e,h,b)['status'],'INCONCLUSIVE')
def test_negative_aggregate_stale_sources(self):
fn,e,h,b=self.aggregate_fixture()
result=fn(e,lambda path:'stale',b);self.assertEqual(result['status'],'INCONCLUSIVE')
for name in ('source-audit','client-provenance','test-receipts','assertion-register','historical-evidence','historical-replay'):
self.assertTrue(any(x.startswith(name+':') for x in result['blockers']))
def test_negative_aggregate_missing_case(self):
fn,e,h,b=self.aggregate_fixture();e['historical-replay']['cases'].pop()
self.assertEqual(fn(e,h,b)['status'],'INCONCLUSIVE')
def test_negative_aggregate_missing_C17(self):
fn,e,h,b=self.aggregate_fixture();e['client-provenance']['commands']=[]
self.assertEqual(fn(e,h,b)['status'],'INCONCLUSIVE')
def test_negative_aggregate_incomplete_coverage(self):
fn,e,h,b=self.aggregate_fixture();e['assertion-coverage']['entries']=0
self.assertEqual(fn(e,h,b)['status'],'INCONCLUSIVE')
# Each generated method has its own executed ID and exact expected contract.
# These are separate negative cases, not a broad 'register valid' receipt.
def install_negative(name,contract,fn):
def test(self):self.reject(contract,lambda:fn(self))
test.__name__='test_negative_'+name
setattr(Case,test.__name__,test)
for name,contract,fn in [
('tag','tag-required',lambda s:Rect('SceneGlobal',0,0,1,1,s.p)),
('integer','integer-geometry',lambda s:Rect(Space.GLOBAL,0.5,0,1,1,s.p)),
('size','nonnegative-size',lambda s:Rect(Space.GLOBAL,0,0,-1,1,s.p)),
('evidence','evidence-required',lambda s:Rect(Space.GLOBAL,0,0,1,1,replace(s.p,evidence=''))),
('assignment_spaces','assignment-spaces',lambda s:content(replace(s.a,window=replace(s.a.window,space=Space.GLOBAL)))),
('native_space','native-space',lambda s:content(replace(s.a,native=replace(s.a.native,rectangle=replace(s.a.native.rectangle,space=Space.GLOBAL))))),
('commit_serial','commit-serial',lambda s:content(replace(s.a,native=replace(s.a.native,commit_serial=0)))),
('assigned_ACK','assigned-configure-ack',lambda s:content(replace(s.a,configure_ack=0))),
('destination','assigned-destination',lambda s:content(replace(s.a,scene=replace(s.a.scene,width=641)))),
('png_from_space','png-to-global-spaces',lambda s:from_png(s.r,s.o)),
('png_from_transform','unmeasured-png-transform',lambda s:from_png(Rect(Space.PNG,0,0,1,1,s.p),replace(s.o,scale=2))),
('paint_area','paint-area',lambda s:verify_paint(s.r,s.o,[482,25,800,598],1,s.clip)),
('popup_spaces','popup-spaces',lambda s:popup(s.r,Rect(Space.GLOBAL,100,80,350,170,s.p),9,9,22,True)),
('crossing_space','crossing-space',lambda s:crossing(replace(s.r,space=Space.PNG),0)),
('local_clip_space','clip-local-space',lambda s:local_clip_to_global(s.clip,(-318,25),s.p)),
('pointer_bounds','pointer-global-bounds',lambda s:pointer_local((1000,1000),s.r,(0,0))),
('standard_owner','standard-owner',lambda s:fresh_standard(s.r,replace(s.r,provenance=replace(s.p,owner=10)))),
('positioner_flags','positioner-flags',lambda s:constraints(64,[0,0,1,1],[0,0,1,1])),
('terminal_codes','actual-terminal-codes',lambda s:terminal(True,None,0,"Handling command 'exit'\nShutting down sway",False,False)),
]:install_negative(name,contract,fn)
# WHY: exercise the production aggregator independently for each mandatory gate.
from write_results import REQUIRED
for gate in REQUIRED:
for mutation in ('missing','failed'):
def test(self,gate=gate,mutation=mutation):
fn,e,h,b=self.aggregate_fixture()
if mutation=='missing':e.pop(gate)
else:e[gate]['status']='FAIL'
result=fn(e,h,b)
self.assertEqual(result['status'],'INCONCLUSIVE')
self.assertTrue(any(x.startswith(gate+':') for x in result['blockers']))
setattr(Case,'test_negative_aggregate_'+gate.replace('-','_')+'_'+mutation,test)
for gate in REQUIRED:
def test(self,gate=gate):
import copy
fn,e,h,b=self.aggregate_fixture()
original=copy.deepcopy(b)
original['evidence_sha256']={n:'reviewed-proof-'+n for n in REQUIRED}
e['independent-review']=dict(status='ACCEPTED',independent=True,**copy.deepcopy(original))
current=copy.deepcopy(original);current['evidence_sha256'][gate]='changed-proof'
result=fn(e,h,current)
self.assertEqual(result['status'],'INCONCLUSIVE')
self.assertTrue(any('review not bound' in x for x in result['blockers']))
setattr(Case,'test_negative_aggregate_'+gate.replace('-','_')+'_stale_review_binding',test)
class Result(unittest.TextTestResult):
def addSuccess(self,test):
super().addSuccess(test);RECEIPTS.append(dict(id=test.id(),status='PASS',mode='negative' if '.test_negative_' in test.id() else 'positive',executed_lines=sorted(LINES.get(test.id(),set())),failed_lines=sorted(FAILED.get(test.id(),set())),contracts=[{'contract':c,'pass':v} for c,v in sorted(CONTRACTS.get(test.id(),set()))]))
def addFailure(self,test,err):
super().addFailure(test,err);RECEIPTS.append(dict(id=test.id(),status='FAIL',error=str(err[1])))
def addError(self,test,err):
super().addError(test,err);RECEIPTS.append(dict(id=test.id(),status='FAIL',error=str(err[1])))
if __name__=='__main__':
parser=argparse.ArgumentParser();parser.add_argument('lab',type=Path);args=parser.parse_args();LAB=args.lab
sys.settrace(trace)
result=unittest.TextTestRunner(verbosity=2,resultclass=Result).run(unittest.defaultTestLoader.loadTestsFromTestCase(Case))
sys.settrace(None)
save(LAB,'test-receipts',dict(source_inventory={str(p):__import__('hashlib').sha256(p.read_bytes()).hexdigest() for p in HERE.iterdir() if p.suffix in ('.py','.patch','.json')},status='PASS' if result.wasSuccessful() else 'FAIL',tests=RECEIPTS))
save(LAB,'positive',{'tests':[r for r in RECEIPTS if r.get('mode')=='positive']})
save(LAB,'negative',{'tests':[r for r in RECEIPTS if r.get('mode')=='negative']})
raise SystemExit(0 if result.wasSuccessful() else 1)

View file

@ -0,0 +1,139 @@
#!/usr/bin/env python3
"""JSON aliases and unsealed independent-review handoff; no runtime authority."""
import argparse
import json
from pathlib import Path
from support import save,sha
HERE=Path(__file__).resolve().parent
REQUIRED=('native-shm','xdg-configure','applied','rendered','positioner',
'historical-evidence','historical-replay','popup-root','popup-nested',
'source-audit','client-provenance','assertion-register',
'assertion-coverage','offline-core-coverage','test-receipts')
def aggregate(evidence,hash_file,bindings):
"""CONTRACT: READY requires complete fresh offline gates and bound review.
WHY: no author test or successful compile can substitute for another gate.
Bindings describe the exact final evidence/source bytes reviewed independently.
"""
failures={}
def need(name,ok,reason):
if not ok:failures.setdefault(name,[]).append(reason)
def fresh(mapping):
return bool(mapping) and all(hash_file(path)==digest for path,digest in mapping.items())
for name in REQUIRED:
d=evidence.get(name)
need(name,isinstance(d,dict) and bool(d),'missing evidence')
if not isinstance(d,dict):continue
status=d.get('status','')
need(name,status=='PASS' or status.startswith('PASS ')
or name=='assertion-register' and status=='CLASSIFIED; execution status is per-entry','gate not PASS')
def record(name):return evidence.get(name) or {}
for name in ('native-shm','xdg-configure','applied','rendered','positioner'):
fields={'native-shm':('size','buffer','stride','format'), 'xdg-configure':('toplevel','initial_ACK','assigned_ACK'),
'applied':('owner','workspace','scene','window','titlebar','globalclip'),
'rendered':('content','PNG_bbox','count','visible_intersection'),
'positioner':('flags','A','B')}[name]
need(name,all(k in record(name) for k in fields),'incomplete geometry proof')
need('historical-evidence',fresh(record('historical-evidence').get('inputs',{})),'stale/missing historical inputs')
cases=record('historical-replay').get('cases',[])
expected={'run-private_mosaic-crossing-b_cross','run-private_mosaic-crossing-both_cross',
'run-private_mosaic-toggle-b_cross','run-private_mosaic-outside-visible',
'run-control-crossing-b_cross','run-control-crossing-both_cross','run-control-outside-visible',
'run-private_mosaic-close_b-visible','run-control-close_b-visible'}
need('historical-replay',len(cases)==9 and {c.get('case') for c in cases}==expected,'required nine cases incomplete')
for c in cases:
need('historical-replay',c.get('status')=='PASS historical sampled replay' and c.get('input_correlation',{}).get('status')=='PASS','case/input proof incomplete')
need('historical-replay',fresh({str(__import__('replay').NESTED/c.get('case','')/n):v for n,v in c.get('files',{}).items()}),'stale case files')
for name in ('popup-root','popup-nested'):
need(name,len(record(name).get('cases',[]))==9,'incomplete popup proof')
audit=record('source-audit');contracts=audit.get('contracts',[])
need('source-audit',len(contracts)==17 and all(c.get('claim') and c.get('excerpts') and hash_file(c.get('source',''))==c.get('sha256') for c in contracts),'incomplete/stale source contracts')
need('source-audit',bool(audit.get('pins')) and hash_file(audit.get('source_version_receipt',''))==audit.get('source_version_sha256') and bool(audit.get('source_version_sha256')),'stale pinned receipt')
client=record('client-provenance');commands=client.get('commands',[])
need('client-provenance',fresh(client.get('inputs',{})),'stale client sources')
need('client-provenance',all(client.get(k) for k in ('patch','adapted_nested','protocols','protocol_comparison','builds')),'incomplete provenance')
needed={n+'-'+mode for n in ('nested-client','pointer-daemon','static-reference') for mode in ('syntax','compile')}
need('client-provenance',needed<={c.get('label') for c in commands} and all(c.get('exit')==0 for c in commands),'C17 commands missing/failed')
for command in commands:
if command.get('label') in needed:need('client-provenance','-std=c17' in command.get('argv',[]) and '-Werror' in command.get('argv',[]),'C17 flags incomplete')
need('client-provenance',hash_file(str(HERE/'placement.patch'))==client.get('patch'),'stale placement patch')
builds={c.get('client'):c for c in client.get('builds',[])}
need('client-provenance',set(builds)=={'nested-client','pointer-daemon','static-reference'},'missing client builds')
for command in commands:
label=command.get('label','');argv=command.get('argv',[])
if label.endswith('-compile') and label[:-8] in builds:
build=builds[label[:-8]]
output=argv[argv.index('-o')+1] if '-o' in argv else ''
source=next((v for v in argv if v.endswith('/'+label[:-8]+'.c')),'')
need('client-provenance',bool(output) and hash_file(output)==build.get('binary') and bool(source) and hash_file(source)==build.get('source'),'stale built client/source')
directory=Path(source).parent
need('client-provenance',all(hash_file(str(directory/n))==v for n,v in client.get('protocols',{}).items()),'stale generated protocols')
register=record('assertion-register');inventory=register.get('source_inventory',{})
need('assertion-register',fresh({str(HERE.parents[2]/p):v for p,v in inventory.items()}) and fresh(register.get('artifact_inventory',{})),'stale inventory')
need('assertion-register',register.get('historical_asserts')==145 and bool(register.get('records')),'incomplete register')
coverage=record('assertion-coverage')
need('assertion-coverage',coverage.get('status')=='PASS' and coverage.get('historical_asserts')==145 and coverage.get('entries')==len(register.get('records',[])) and coverage.get('unresolved_pure_invariants')==[],'coverage incomplete')
need('offline-core-coverage',record('offline-core-coverage').get('unproved')==[],'core unproved')
tests=record('test-receipts');receipts=tests.get('tests',[])
need('test-receipts',fresh(tests.get('source_inventory',{})),'stale test sources')
need('test-receipts',bool(receipts) and all(t.get('status')=='PASS' for t in receipts) and len({t.get('id') for t in receipts})==len(receipts),'missing/failed test receipts')
review=record('independent-review')
need('independent-review',review.get('status')=='ACCEPTED' and review.get('independent') is True,'review not independently ACCEPTED')
need('independent-review',bool(bindings.get('source_delta')) and bool(bindings.get('evidence_sha256')) and all(review.get(k)==v for k,v in bindings.items()),'review not bound to final source/evidence hashes')
groups={'STATIC_NESTED_SHM_RENDER_GEOMETRY_REPLAY':('native-shm','applied','rendered','historical-evidence'),
'STATIC_NESTED_XDG_GEOMETRY_AUDIT':('xdg-configure','positioner','historical-replay','popup-root','popup-nested','source-audit','client-provenance'),
'STATIC_NESTED_ASSERTION_COVERAGE':('assertion-register','assertion-coverage','offline-core-coverage'),
'STATIC_NESTED_OFFLINE_REGRESSIONS':('test-receipts',),
'STATIC_NESTED_INDEPENDENT_REVIEW':('independent-review',)}
markers={key:'PASS' if not any(n in failures for n in names) else 'INCONCLUSIVE' for key,names in groups.items()}
return dict(status='INCONCLUSIVE' if failures else 'READY_FOR_NEW_RUNTIME',markers=markers,
marker_scope={key:list(names) for key,names in groups.items()},
blockers=[name+': '+reason for name,reasons in failures.items() for reason in reasons],review_bindings=bindings)
def write(lab):
results=lab/'results'
def read(name):
path=results/(name+'.json')
return json.loads(path.read_text()) if path.exists() else {}
aliases={'native-shm-geometry':'native-shm','xdg-configure-geometry':'xdg-configure','applied-content-geometry':'applied','rendered-paint-geometry':'rendered','popup-positioner-audit':'positioner','historical-popup-replay':'historical-replay','root-clip-model':'popup-root','nested-clip-model':'popup-nested','positive-tests':'positive','negative-tests':'negative'}
for name,source in aliases.items():save(lab,name,read(source))
coverage=read('assertion-coverage');tests=read('test-receipts');core=read('offline-core-coverage')
reviewfile=results/'independent-review.json'
review=read('independent-review') if reviewfile.exists() else {'status':'NOT RUN','independent':False}
evidence={name:read(name) for name in REQUIRED}
evidence['independent-review']=review
source_delta={p.name:sha(p) for p in HERE.iterdir() if p.is_file()}
bindings=dict(source_delta=source_delta,evidence_sha256={name:sha(results/(name+'.json')) for name in REQUIRED if (results/(name+'.json')).exists()})
def safe_hash(path):
try:return sha(path)
except (OSError,ValueError):return None
gates=aggregate(evidence,safe_hash,bindings)
markers=gates['markers'];blockers=gates['blockers'];status=gates['status']
save(lab,'popup-geometry-model',dict(status=markers['STATIC_NESTED_XDG_GEOMETRY_AUDIT'],scope='offline typed model and sampled historical replay; new runtime NOT TESTED',root=read('popup-root'),nested=read('popup-nested'),prediction=read('positioner'),source='source-audit.json',native_input='Opening click must lie in actual native surface bounds; destination scaling alone is insufficient'))
readiness=dict(status=status,marker='SWAYFX_MOSAIC_STATIC_NESTED_GEOMETRY_OFFLINE_GATE='+status,markers=markers,marker_scope=gates['marker_scope'],review_bindings=bindings,blockers=blockers,runtime='NOT TESTED',architectural_conclusion='UNDECIDED',fixture_only=True,current_ticket_runtime_authorized=False,runtime_budget_initialized=False,independent_review=review)
save(lab,'runner-readiness',readiness);save(lab,'offline-gate',readiness)
save(lab,'summary',dict(status=status,markers=markers,tests=len(tests.get('tests',[])),coverage=coverage,core=core,historical_cases=len(read('historical-replay').get('cases',[])),runtime_runs=0,new_popups=0,new_grabs=0,new_captures=0,new_camera_operations=0,runtime_budget_initialized=False,production_changes=False,source_delta={p.name:sha(p) for p in HERE.iterdir() if p.is_file()},manifest='UNSEALED; parent review required',next='independent review of final fixture/register/evidence; separate future authorization required for runtime',limitations=['atomic transaction-generation/native-buffer-frame identity NOT PROVEN','new static popup crossing/grab/input/standard NOT TESTED','vertical/scaled/rotated/migration/full damage NOT TESTED','production cross-output viewport NOT YET SUPPORTED']))
(lab/'independent-review-input.md').write_text('''# Independent review input — EXPERIMENTAL
Review this final fixture against the offline gate; review E1/E2, actual
configure/ACK/map/grab, typed geometry, native input bounds, root correlation,
standard fresh origin, dismissal, terminal and owned cleanup.
Inputs: repository fixture sources, results/source-audit.json,
source-versions.json, historical-evidence.json, historical-popup-replay.json,
assertion-register.json, assertion-coverage.json, offline-core-coverage.json,
test-receipts.json, client-provenance.json and runner-readiness.json.
Write independent-review.md and results/independent-review.json with
ACCEPTED/CORRECTION_REQUIRED/NOT PROVEN findings. No author review PASS, runtime
launch, budget initialization or manifest sealing is authorized here.
''')
print(json.dumps(readiness,indent=2))
if __name__=='__main__':
parser=argparse.ArgumentParser();parser.add_argument('lab',type=Path);write(parser.parse_args().lab)