1	import Base
2	import ./execution_composer_layout.bend as Layout
3	import ./execution_command_permission.bend as Permission
4	import ./execution_relation_provider.bend as GraphProvider
5	import ./execution_lifetime_scope_provider.bend as ScopeProvider
6	import ./execution_relation_store.bend as GraphStore
7	import ./execution_lifetime_scope_store.bend as ScopeStore
8	import ./execution_relation_failure_retention.bend as Retention
9	import ./execution_resource_policy.bend as Policy
10	import ./relation_types.bend as T
11	import ./execution_relation_context.bend as Context
12	
13	# A provisioning declaration constructs its owner and framework maintenance
14	# evidence together. It grants no capability to an executing gameplay body.
15	type Blueprint<-S:Data,-resources:Layout.Layout,-Seed:Type> is Type:
16	  Blueprint{build:U32 -> Seed -> Layout.resources(~S,resources),graphs:List<&2,Layout.Route>,scopes:List<&2,Layout.Route>,selection:Permission.Selection<S,resources>,retention:Retention.Program(~S,~resources),preflight:U32 -> Layout.resources(~S,resources) -> Layout.resources(~S,resources) & Bool}
17	type Bound<-S:Data,-WR:Type,-resources:Layout.Layout,-same:{WR == Layout.resources(~S,resources) : Type},-Seed:Type,-blueprint:Blueprint<S,resources,Seed>,-Application:Type> is Type:
18	  Bound{bound:Context.Bound<S,WR,resources,same,Application>}
19	def reported(~S:Data,~WR:Type,~resources:Layout.Layout,~same:{WR == Layout.resources(~S,resources) : Type},~Seed:Type,~blueprint:Blueprint<S,resources,Seed>,-Application:Type,-Report:Data,result:Context.Bound<S,WR,resources,same,Application> & Report) -> Bound<S,WR,resources,same,Seed,blueprint,Application> & Report:
20	  match result:
21	    case (bound,report):(Bound{bound},report)
22	def unchecked(~S:Data,~resources:Layout.Layout,_:U32,owners:Layout.resources(~S,resources)) -> Layout.resources(~S,resources) & Bool:
23	  (owners,True{})
24	def graph_preflight(~S:Data,~descriptor:T.Descriptor<S>,~key:String,expected:U32,owners:Layout.resources(~S,GraphProvider.layout(~S,~descriptor,key))) -> Layout.resources(~S,GraphProvider.layout(~S,~descriptor,key)) & Bool:
25	  match owners:
26	    case Layout.ResourceSlot{Layout.Viewed{GraphStore.Store{+namespace,graph,failures,sequence,nextReader},cache},stamp}:(Layout.ResourceSlot{Layout.Viewed{GraphStore.Store{namespace,graph,failures,sequence,nextReader},cache},stamp},U32.is_eq(expected,namespace))
27	def scope_preflight(~S:Data,~key:String,expected:U32,owners:Layout.resources(~S,ScopeProvider.layout(~S,key))) -> Layout.resources(~S,ScopeProvider.layout(~S,key)) & Bool:
28	  match owners:
29	    case Layout.ResourceSlot{Layout.Viewed{ScopeStore.Store{+namespace,members},cache},stamp}:(Layout.ResourceSlot{Layout.Viewed{ScopeStore.Store{namespace,members},cache},stamp},U32.is_eq(expected,namespace))
30	
31	def ordinary_layout(~P:Type,~V:Data,~refresh:P -> P & V,key:String) -> Layout.Layout:
32	  Layout.LayoutLeaf{P,V,refresh,key,Policy.Ordinary{}}
33	def ordinary_owner(~S:Data,~P:Type,~V:Data,~refresh:P -> P & V,~key:String,_:U32,owner:P) -> Layout.resources(~S,ordinary_layout(~P,~V,~refresh,key)):
34	  Layout.ResourceSlot{Layout.initialize(ordinary_layout(~P,~V,~refresh,key),Layout.AtLeaf{},owner),Layout.unknown_stamp()}
35	def ordinary(~S:Data,~P:Type,~V:Data,~refresh:P -> P & V,~key:String) -> Blueprint<S,ordinary_layout(~P,~V,~refresh,key),P>:
36	  Blueprint{ordinary_owner(~S,~P,~V,~refresh,~key),[],[],Permission.no_selection(~S,~ordinary_layout(~P,~V,~refresh,key)),Retention.empty(~S,~ordinary_layout(~P,~V,~refresh,key)),unchecked(~S,~ordinary_layout(~P,~V,~refresh,key))}
37	def graph_owner(~S:Data,~descriptor:T.Descriptor<S>,~key:String,namespace:U32,_:Unit) -> Layout.resources(~S,GraphProvider.layout(~S,~descriptor,key)):
38	  Layout.ResourceSlot{Layout.initialize(GraphProvider.layout(~S,~descriptor,key),Layout.AtLeaf{},GraphStore.fresh(~S,~descriptor,namespace)),Layout.unknown_stamp()}
39	def graph(~S:Data,~descriptor:T.Descriptor<S>,~key:String) -> Blueprint<S,GraphProvider.layout(~S,~descriptor,key),Unit>:
40	  Blueprint{graph_owner(~S,~descriptor,~key),[Layout.AtLeaf{}],[],Permission.extend_selection(~S,~GraphProvider.layout(~S,~descriptor,key),~Layout.AtLeaf{},~{==},~descriptor,~{==},~{==},~{==},Permission.no_selection(~S,~GraphProvider.layout(~S,~descriptor,key))),Retention.extend(~S,~GraphProvider.layout(~S,~descriptor,key),~Layout.AtLeaf{},~{==},~descriptor,~{==},~{==},~{==},Retention.empty(~S,~GraphProvider.layout(~S,~descriptor,key))),graph_preflight(~S,~descriptor,~key)}
41	def scope_owner(~S:Data,~key:String,namespace:U32,_:Unit) -> Layout.resources(~S,ScopeProvider.layout(~S,key)):
42	  Layout.ResourceSlot{Layout.initialize(ScopeProvider.layout(~S,key),Layout.AtLeaf{},ScopeStore.fresh(~S,namespace)),Layout.unknown_stamp()}
43	def scope(~S:Data,~key:String) -> Blueprint<S,ScopeProvider.layout(~S,key),Unit>:
44	  Blueprint{scope_owner(~S,~key),[],[Layout.AtLeaf{}],Permission.extend_scope_selection(~S,~ScopeProvider.layout(~S,key),~Layout.AtLeaf{},~{==},~{==},~{==},~{==},Permission.no_selection(~S,~ScopeProvider.layout(~S,key))),Retention.empty(~S,~ScopeProvider.layout(~S,key)),scope_preflight(~S,~key)}
45	def builder(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> U32 -> Seed -> Layout.resources(~S,resources):
46	  match value:
47	    case Blueprint{build,_,_,_,_,_}: build
48	def graphs(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> List<&2,Layout.Route>:
49	  match value:
50	    case Blueprint{_,graphs,_,_,_,_}: graphs
51	def scopes(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> List<&2,Layout.Route>:
52	  match value:
53	    case Blueprint{_,_,scopes,_,_,_}: scopes
54	def selection(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> Permission.Selection<S,resources>:
55	  match value:
56	    case Blueprint{_,_,_,selection,_,_}: selection
57	def retention(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> Retention.Program(~S,~resources):
58	  match value:
59	    case Blueprint{_,_,_,_,retention,_}: retention
60	def cleanup(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> Permission.CleanupSelection<S,resources>:
61	  match value:
62	    case Blueprint{_,graphs,scopeRoutes,Permission.Selection{program,snapshot,scopes,_},_,_}: Permission.Provisioned{program,snapshot,scopes,graphs,scopeRoutes}
63	def preflight(~S:Data,~resources:Layout.Layout,~Seed:Type,value:Blueprint<S,resources,Seed>) -> U32 -> Layout.resources(~S,resources) -> Layout.resources(~S,resources) & Bool:
64	  match value:
65	    case Blueprint{_,_,_,_,_,preflight}:preflight