Appendix B · The five proofs on one page

TaskHarbor identities: ada c3c3c3c3-c3c3-c3c3-c3c3-c3c3c3c3c3c3 (Aster owner) · bo d4d4d4d4-d4d4-d4d4-d4d4-d4d4d4d4d4d4 (Borealis owner) · eve e5e5e5e5-e5e5-e5e5-e5e5-e5e5e5e5e5e5 (Aster member). Aster workspace a1a1a1a1-a1a1-a1a1-a1a1-a1a1a1a1a1a1, its project …a1a2; Borealis project b2b2b2b2-b2b2-b2b2-b2b2-b2b2b2b2b2b3. Full CI-ready versions: Chapter 6.

P1 · Read isolation — bo must see his own task and none of Aster's:

begin;
set local role authenticated;
set local request.jwt.claim.sub = 'd4d4d4d4-d4d4-d4d4-d4d4-d4d4d4d4d4d4';
select count(*) as visible,
       count(*) filter (where project_id = 'a1a1a1a1-a1a1-a1a1-a1a1-a1a1a1a1a1a2') as aster
from public.tasks;                       -- expected: visible = 1, aster = 0
rollback;

P2 · Insert fence — eve cannot write into Borealis (must raise 42501):

begin;
set local role authenticated;
set local request.jwt.claim.sub = 'e5e5e5e5-e5e5-e5e5-e5e5-e5e5e5e5e5e5';
insert into public.tasks (project_id, title)
values ('b2b2b2b2-b2b2-b2b2-b2b2-b2b2b2b2b2b3', 'smuggled');  -- expected: ERROR 42501
rollback;

P3 · Update immobility — bo silently changes nothing in Aster (using filters first):

begin;
set local role authenticated;
set local request.jwt.claim.sub = 'd4d4d4d4-d4d4-d4d4-d4d4-d4d4d4d4d4d4';
update public.tasks set title = 'hijacked'
where project_id = 'a1a1a1a1-a1a1-a1a1-a1a1-a1a1a1a1a1a2'
returning id;                            -- expected: zero rows, no error
rollback;

P4 · Delete fence — bo deletes nothing in Aster:

begin;
set local role authenticated;
set local request.jwt.claim.sub = 'd4d4d4d4-d4d4-d4d4-d4d4-d4d4d4d4d4d4';
delete from public.tasks
where project_id = 'a1a1a1a1-a1a1-a1a1-a1a1-a1a1a1a1a1a2'
returning 1;                             -- expected: zero rows, no error
rollback;

P5 · Revocation — removing a member closes access immediately (was 2, now 0):

begin;
delete from public.members
 where workspace_id = 'a1a1a1a1-a1a1-a1a1-a1a1-a1a1a1a1a1a1'
   and user_id      = 'e5e5e5e5-e5e5-e5e5-e5e5-e5e5e5e5e5e5';
set local role authenticated;
set local request.jwt.claim.sub = 'e5e5e5e5-e5e5-e5e5-e5e5-e5e5e5e5e5e5';
select count(*) from public.tasks;       -- expected: 0
rollback;

Adaptation rule: keep the three-part shape — identity (set local role + claim), one statement, one expected outcome — and assert counts for filtered operations, throws_ok-style errors for rejected writes. Seed known data first so a zero always means "filtered," never "empty table."