1	import Base
2	import ./execution_effects.bend as E
3	import ./execution_state_effect.bend as StateEffect
4	import ./execution_lifetime_scope_buffer.bend as LifetimeScope
5	import ./execution_reservation_authority.bend as Effect
6	import ./execution_reservation_authority.bend as Request
7	import ./world.bend as W
8	import ./execution_system.bend as Sys
9	import ./execution_builder.bend as Build
10	import ./execution_system_registration.bend as Registration
11	import ./execution_composer_layout.bend as Layout
12	import ./execution_command_local.bend as Local
13	import ./execution_command_buffer.bend as Buffer
14	import ./execution_command_publication.bend as Publication
15	import ./change_tick.bend as Tick
16	import ./execution_command_permission.bend as Permission
17	import ./execution_command_removed.bend as Removed
18	import ./execution_declaration.bend as D
19	import ./execution_state.bend as State
20	import ./execution_relation_context.bend as Context
21	
22	# Command owners have a distinct type, so an ordinary Sys.Owner leaf cannot
23	# silently omit their deferred inventory and publication operation.
24	def ScopedOps(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,Permit:Data,F:Type -> Type,H:Type) -> Type:
25	  Permission.Prepared<Ops(Permit,F,H,Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>),S,resources>
26	def Program(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type) -> Type:
27	  @-Permit:Data -> @-F:(Type -> Type) -> @-effects:E.Effects<F> -> @-H:Type -> @-Q:Type -> @-commands:Local.Commands<Q,S,Layout.payload(layout,route)> -> @-B:Type -> @-builder:Build.Builder(~S,~(Layout.columns(~S,layout)),~C,~R,~Permit,~F,~H,~B) -> @-K:Type -> @-entity:Permission.Grant(~S,~layout,~Permit,~F,~Q,~K) -> @-relations:Permission.RelationGrant(~S,~resources,~Q,~K) -> @-scopes:Permission.ScopeGrant(~S,~resources,~Q,~K) -> B -> K -> B & (K & Ops(Permit,F,H,Q))
28	def program_for_buffer(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~Permit:Data,~token:Permit,~F:Type -> Type,~effects:E.Effects<F>,~request:Permit -> F(W.Reservation<S>),~H:Type,~B:Type,~builder:Build.Builder(~S,~(Layout.columns(~S,layout)),~C,~R,~Permit,~F,~H,~B),book:B) -> B & ScopedOps(~S,~layout,~resources,~route,~Ops,Permit,F,H):
29	  Permission.prepared(~S,~layout,~resources,B,Ops(Permit,F,H,Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>),declaration(Permit,F,effects,H,Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>,Local.canonical(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout))),B,builder,Permission.Book<S,layout,resources>,Permission.grant(~S,~layout,~resources,~Permit,~F,~(Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>),~(Buffer.despawn(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)))),~(Buffer.spawn(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)),~Permit,~F,~effects,~token,~request))),Permission.relation_grant(~S,~layout,~resources,~Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>,~Buffer.relation(~S,~Layout.payload(layout,route),~Removed.Removed(layout))),Permission.scope_grant(~S,~layout,~resources,~Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>,~Buffer.lifetime_scope(~S,~Layout.payload(layout,route),~Removed.Removed(layout))),book,Permission.fresh(~S,~layout,~resources)))
30	
31	def Body(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data) -> Type:
32	  @-Permit:Data -> @-F:(Type -> Type) -> @-effects:E.Effects<F> -> @-H:Type -> @-Q:Type -> @-caps:Ops(Permit,F,H,Q) -> @-commands:Local.Commands<Q,S,Layout.payload(layout,route)> -> H -> Q -> User -> F(H & (Q & (User & Sys.Completion<Error,Out>)))
33	def Captures(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~User:Type) -> Type:
34	  Local.Local<S,Layout.payload(layout,route),Removed.Removed(layout),User>
35	def prepared_permission(~S:Data,~resources:Layout.Layout,-Ops:Type,value:Permission.Prepared<Ops,S,resources>) -> Permission.Permission:
36	  match value:
37	    case Permission.Prepared{permission,relations,_,_}:permission
38	type CheckedPermission<-S:Data,-resources:Layout.Layout> is Data:
39	  ReadyPermission{permission:Permission.Permission,relations:Permission.Relations<S,resources>}
40	  UnsupportedPermission{permission:Permission.Permission,relations:Permission.Relations<S,resources>}
41	def compiled_permission(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,value:D.Compilation<S,Layout.columns(~S,layout),C,R,ScopedOps(~S,~layout,~resources,~route,~Ops)>) -> CheckedPermission<S,resources>:
42	  match value:
43	    case D.Supported{D.Declaration{Permission.Prepared{permission,relations,_,_},_},_}:ReadyPermission{permission,relations}
44	    case D.Unsupported{Permission.Prepared{permission,relations,_,_},_,_}:UnsupportedPermission{permission,relations}
45	def inspect_permission(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,value:D.Compilation<S,Layout.columns(~S,layout),C,R,ScopedOps(~S,~layout,~resources,~route,~Ops)>) -> D.Compilation<S,Layout.columns(~S,layout),C,R,ScopedOps(~S,~layout,~resources,~route,~Ops)> & CheckedPermission<S,resources>:
46	  match value:
47	    case D.Supported{D.Declaration{Permission.Prepared{+permission,+relations,selection,ops},access},recipes}:(D.Supported{D.Declaration{Permission.Prepared{permission,relations,selection,ops},access},recipes},ReadyPermission{permission,relations})
48	    case D.Unsupported{Permission.Prepared{+permission,+relations,selection,ops},access,recipes}:(D.Unsupported{Permission.Prepared{permission,relations,selection,ops},access,recipes},UnsupportedPermission{permission,relations})
49	# Static construction projection only. Ordinary barriers retain and inspect the
50	# actual Compilation; they never invoke this projection on its affine caps.
51	def construction_selection(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,value:D.Compilation<S,Layout.columns(~S,layout),C,R,ScopedOps(~S,~layout,~resources,~route,~Ops)>) -> Permission.Selection<S,resources>:
52	  match value:
53	    case D.Supported{D.Declaration{Permission.Prepared{_,_,selection,_},_},_}:selection
54	    case D.Unsupported{Permission.Prepared{_,_,selection,_},_,_}:selection
55	def declared_permission(~S:Data,~C:Type,~R:Type,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops)) -> CheckedPermission<S,resources>:
56	  compiled_permission(~S,~C,~R,~layout,~resources,~route,~Ops,Build.compile_framework(~S,~(Layout.columns(~S,layout)),~C,~R,~ScopedOps(~S,~layout,~resources,~route,~Ops),~program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration)))
57	def checked_permission_agrees(~S:Data,~resources:Layout.Layout,permission:Permission.Permission,checked:CheckedPermission<S,resources>) -> Bool:
58	  match checked:
59	    case ReadyPermission{expected,_}:Permission.agrees(permission,expected)
60	    case UnsupportedPermission{_,_}:False{}
61	def checked_relations(~S:Data,~resources:Layout.Layout,checked:CheckedPermission<S,resources>) -> Permission.Relations<S,resources>:
62	  match checked:
63	    case ReadyPermission{_,relations}:relations
64	    case UnsupportedPermission{_,relations}:relations
65	def checked_deferred_descriptions(~S:Data,~resources:Layout.Layout,checked:CheckedPermission<S,resources>) -> List<&2,Permission.DeferredRelation<S>>:
66	  Permission.deferred_descriptions(~S,~resources,checked_relations(~S,~resources,checked))
67	
68	def runner(~S:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~Permit:Data,~F:Type -> Type,~effects:E.Effects<F>,~H:Type,~caps:ScopedOps(~S,~layout,~resources,~route,~Ops,Permit,F,H),scope:H,local:Captures(~S,~layout,~resources,~route,~User)) -> F(H & (Captures(~S,~layout,~resources,~route,~User) & Sys.Completion<Error,Out>)):
69	  Local.invoke(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)),~Permit,~F,~effects,~User,~Error,~Out,~Ops,~body,~H,~(Permission.ops_field(Ops(Permit,F,H,Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>),S,resources,caps)),scope,local)
70	def System(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out)) -> Type:
71	  Sys.Owner<S,Layout.columns(~S,layout),C,R,E,ScopedOps(~S,~layout,~resources,~route,~Ops),Captures(~S,~layout,~resources,~route,~User),Error,Out,program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body)>
72	type Owner<-S:Data,-C:Type,-R:Type,-E:Data,-layout:Layout.Layout,-resources:Layout.Layout,-route:Layout.Route,-Ops:Data -> (Type -> Type) -> Type -> Type -> Type,-User:Type,-Error:Data,-Out:Data,-declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),-body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out)> is Type:
73	  Owner{system:Sys.Owner<S,Layout.columns(~S,layout),C,R,E,ScopedOps(~S,~layout,~resources,~route,~Ops),Captures(~S,~layout,~resources,~route,~User),Error,Out,program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body)>}
74	def wrapped(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,result:Sys.Defined<W.World<S,Layout.columns(~S,layout),WR,E>,Sys.Owner<S,Layout.columns(~S,layout),C,R,E,ScopedOps(~S,~layout,~resources,~route,~Ops),Captures(~S,~layout,~resources,~route,~User),Error,Out,program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body)>,Captures(~S,~layout,~resources,~route,~User)>) -> Sys.Defined<W.World<S,Layout.columns(~S,layout),WR,E>,Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Captures(~S,~layout,~resources,~route,~User)>:
75	  match result:
76	    case Sys.Defined{world,system}:Sys.Defined{world,Owner{system}}
77	    case Sys.DefinitionRefused{world,local}:Sys.DefinitionRefused{world,local}
78	
79	# The full command schema fixes the inserted payload type and destination.
80	# C/R describe the physical gameplay scope, which may be one root-cut branch;
81	# registration always uses the actual complete World and its single allocator.
82	def define_checked(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,world:W.World<S,Layout.columns(~S,layout),WR,E>,name:String,user:User,checked:CheckedPermission<S,resources>) -> Sys.Defined<W.World<S,Layout.columns(~S,layout),WR,E>,Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Captures(~S,~layout,~resources,~route,~User)>:
83	  match checked:
84	    case UnsupportedPermission{permission,relations}:Sys.DefinitionRefused{world,Local.fresh(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)),~User,user,permission)}
85	    case ReadyPermission{permission,relations}:wrapped(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,Registration.define_framework(~S,~(Layout.columns(~S,layout)),~C,~R,~E,~ScopedOps(~S,~layout,~resources,~route,~Ops),~Captures(~S,~layout,~resources,~route,~User),~Error,~Out,~program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),~runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body),~WR,world,name,Local.fresh(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)),~User,user,permission)))
86	def define(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,world:W.World<S,Layout.columns(~S,layout),WR,E>,name:String,user:User) -> Sys.Defined<W.World<S,Layout.columns(~S,layout),WR,E>,Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Captures(~S,~layout,~resources,~route,~User)>:
87	  define_checked(~S,~C,~R,~E,~layout,~resources,~route,~valid,~Ops,~User,~Error,~Out,~declaration,~body,~WR,world,name,user,declared_permission(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration))
88	
89	type Metadata is Data:
90	  Metadata{id:U32,component:String,permission:Permission.Permission}
91	def metadata(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),owner:Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Metadata:
92	  match owner:
93	    case Owner{Sys.Owner{namespace,+id,name,access,cursor,Local.Local{user,commands,+permission}}}:(Owner{Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,permission}}},Metadata{id,Layout.key(layout,route),permission})
94	
95	def pending_returned(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),meta:Registration.Meta<System(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body)>,user:User,permission:Permission.Permission,result:Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)> & Bool) -> Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
96	  match result:
97	    case (commands,pending):(Owner{Registration.restored(~S,~(Layout.columns(~S,layout)),~C,~R,~E,~ScopedOps(~S,~layout,~resources,~route,~Ops),~Captures(~S,~layout,~resources,~route,~User),~Error,~Out,~program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),~runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body),meta,Local.Local{user,commands,permission})},pending)
98	def pending(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),owner:Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
99	  match owner:
100	    case Owner{Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,permission}}}:pending_returned(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,Registration.Meta{namespace,id,name,access,cursor},user,permission,Buffer.pending(~S,~(Layout.payload(layout,route)),~(Removed.Removed(layout)),commands))
101	def published(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,meta:Registration.Meta<System(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body)>,user:User,permission:Permission.Permission,result:W.World<S,Layout.columns(~S,layout),WR,E> & Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>) -> W.World<S,Layout.columns(~S,layout),WR,E> & Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
102	  match result:
103	    case (world,commands):(world,Owner{Registration.restored(~S,~(Layout.columns(~S,layout)),~C,~R,~E,~ScopedOps(~S,~layout,~resources,~route,~Ops),~Captures(~S,~layout,~resources,~route,~User),~Error,~Out,~program_for_buffer(~S,~C,~R,~layout,~resources,~route,~Ops,~declaration),~runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body),meta,Local.Local{user,commands,permission})})
104	# These gates consume the closed action once and preserve each affine owner.
105	def publication_gate(-World:Type,-Owner:Type,allowed:Bool,world:World,owner:Owner,apply:World -> Owner -> World & Owner) -> World & Owner:
106	  match allowed:
107	    case False{}:(world,owner)
108	    case True{}:apply(world,owner)
109	def publication_verified_gate(-World:Type,-Commands:Type,-Owner:Type,result:World & Bool,commands:Commands,coherent:Unit -> Bool,apply:World -> Commands -> World & Commands,restore:World & Commands -> World & Owner) -> World & Owner:
110	  match result:
111	    case (world,allowed):restore(publication_gate(World,Commands,Bool.and(coherent(Unit{}),allowed),world,commands,apply))
112	def publish_interpreted(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,~scopeInterpreter:LifetimeScope.Interpreter(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR),+checked:CheckedPermission<S,resources>,tick:Tick.Tick,world:W.World<S,Layout.columns(~S,layout),WR,E>,owner:Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,Layout.columns(~S,layout),WR,E> & Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
113	  match owner:
114	    case Owner{Sys.Owner{+namespace,+id,+name,+access,+cursor,Local.Local{user,commands,+permission}}}:publication_verified_gate(W.World<S,Layout.columns(~S,layout),WR,E>,Buffer.Buffer<S,Layout.payload(layout,route),Removed.Removed(layout)>,Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>,Registration.verify(~S,~(Layout.columns(~S,layout)),~WR,~E,~System(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),Registration.Meta{namespace,id,name,access,cursor},world),commands,_ => Bool.and(checked_permission_agrees(~S,~resources,permission,checked),Permission.relations_agree(~S,~resources,relations,checked_relations(~S,~resources,checked))),actionWorld => actionCommands => Publication.apply_at_interpreted(~S,~WR,~E,~layout,~route,~valid,~resources,~sameWR,~selection,~relations,~scopeInterpreter,Context.Context{namespace},permission,actionWorld,actionCommands,tick),published(~S,~C,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~WR,Registration.Meta{namespace,id,name,access,cursor},user,permission))
115	
116	# Raw constructors are trusted administrative provisioning. Canonical admission
117	# validates the persisted cache against this owner's same closed declaration;
118	# no World payload is projected and no separately supplied catalog is consulted.
119	def permission_matches(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),checked:CheckedPermission<S,resources>,owner:Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body> & Bool:
120	  match owner:
121	    case Owner{Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,+permission}}}:(Owner{Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,permission}}},checked_permission_agrees(~S,~resources,permission,checked))
122	
123	def admitted_grant(permission:Permission.Permission) -> Request.Grant:
124	  match permission:
125	    case Permission.FamilyOnly{}:Request.NoStructural{}
126	    case Permission.EntityStructural{}:Request.Structural{}
127	def trusted_run_agreed(~S:Data,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~Layout.columns(~S,layout),~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~caps:ScopedOps(~S,~layout,~resources,~route,~Ops,Effect.Granted,StateEffect.Transition(~State.Invocation<S>),State.Scope<S,Layout.columns(~S,layout),R>),allowed:Bool,grant:Request.Grant,compilation:D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)>,system:System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),world:W.World<S,Layout.columns(~S,layout),R,E>) -> D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)> & Sys.RunResult<W.World<S,Layout.columns(~S,layout),R,E>,System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),Error,Out>:
128	  match allowed:
129	    case False{}:(compilation,Sys.Refused{world,system})
130	    case True{}:Sys.trusted_run_retained_compilation(~S,~Layout.columns(~S,layout),~R,~E,~ScopedOps(~S,~layout,~resources,~route,~Ops),~Captures(~S,~layout,~resources,~route,~User),~Error,~Out,~program_for_buffer(~S,~Layout.columns(~S,layout),~R,~layout,~resources,~route,~Ops,~declaration),~runner(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out,~body),~caps,grant,compilation,system,world)
131	def trusted_run_inspected(~S:Data,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~Layout.columns(~S,layout),~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~caps:ScopedOps(~S,~layout,~resources,~route,~Ops,Effect.Granted,StateEffect.Transition(~State.Invocation<S>),State.Scope<S,Layout.columns(~S,layout),R>),system:System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),world:W.World<S,Layout.columns(~S,layout),R,E>,inspected:D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)> & CheckedPermission<S,resources>) -> D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)> & Sys.RunResult<W.World<S,Layout.columns(~S,layout),R,E>,System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),Error,Out>:
132	  match system inspected:
133	    case system Tuple{compilation,UnsupportedPermission{_,_}}:(compilation,Sys.Refused{world,system})
134	    case Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,+actual}} Tuple{compilation,ReadyPermission{+expected,_}}:trusted_run_agreed(~S,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~caps,Permission.agrees(actual,expected),admitted_grant(expected),compilation,Sys.Owner{namespace,id,name,access,cursor,Local.Local{user,commands,actual}},world)
135	def run_retained_system(~S:Data,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~Layout.columns(~S,layout),~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~caps:ScopedOps(~S,~layout,~resources,~route,~Ops,Effect.Granted,StateEffect.Transition(~State.Invocation<S>),State.Scope<S,Layout.columns(~S,layout),R>),compilation:D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)>,system:System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),world:W.World<S,Layout.columns(~S,layout),R,E>) -> D.Compilation<S,Layout.columns(~S,layout),Layout.columns(~S,layout),R,ScopedOps(~S,~layout,~resources,~route,~Ops)> & Sys.RunResult<W.World<S,Layout.columns(~S,layout),R,E>,System(~S,~Layout.columns(~S,layout),~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body),Error,Out>:
136	  trusted_run_inspected(~S,~R,~E,~layout,~resources,~route,~Ops,~User,~Error,~Out,~declaration,~body,~caps,system,world,inspect_permission(~S,~Layout.columns(~S,layout),~R,~layout,~resources,~route,~Ops,compilation))
137	
138	def publish(~S:Data,~C:Type,~R:Type,~E:Data,~layout:Layout.Layout,~resources:Layout.Layout,~route:Layout.Route,~valid:{Layout.grant_valid(~layout,~route) == True{} : Bool},~Ops:Data -> (Type -> Type) -> Type -> Type -> Type,~User:Type,~Error:Data,~Out:Data,~declaration:Program(~S,~C,~R,~layout,~resources,~route,~Ops),~body:Body(~S,~layout,~resources,~route,~Ops,~User,~Error,~Out),~WR:Type,~sameWR:{WR == Layout.resources(~S,resources) : Type},~relations:Permission.Relations<S,resources>,~selection:Permission.Selection<S,resources>,checked:CheckedPermission<S,resources>,tick:Tick.Tick,world:W.World<S,Layout.columns(~S,layout),WR,E>,owner:Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>) -> W.World<S,Layout.columns(~S,layout),WR,E> & Owner<S,C,R,E,layout,resources,route,Ops,User,Error,Out,declaration,body>:
139	  publish_interpreted(~S,~C,~R,~E,~layout,~resources,~route,~valid,~Ops,~User,~Error,~Out,~declaration,~body,~WR,~sameWR,~relations,~selection,~LifetimeScope.apply(~S,~Layout.columns(~S,layout),~WR,~E,~Layout.payload(layout,route),~Removed.Removed(layout),~resources,~sameWR,~selection,~relations,~Publication.scope_dispose(~S,~WR,~E,~layout,~route)),checked,tick,world,owner)