capabilities.bend
1import Base
2import component.bend as Cmp
3
4# Closed declaration bundles contain operations, never runtime-owned storage.
5# Gameplay specializes field projections while threading one abstract owner.
6# Component read capability: threads opaque owner H and returns Access<V>.
7# V is detached Data; no affine payload owner or setter is exposed.
8type Read<-H: Type,-V: Data> is Type:
9 Read{get: H -> H & Cmp.Access<V>}
10# Component read/replacement capability. set consumes payload C and returns
11# H; it does not itself return rejected C. The bound operation defines error
12# recording and rollback. Raw constructors are trusted operation adapters.
13type Write<-H: Type,-C: Type,-V: Data> is Type:
14 Write{get: H -> H & Cmp.Access<V>,set: H -> C -> H}
15# Heterogeneous pair of grants for the same application capability shape.
16# Contains operations, not live World storage; nest for additional grants.
17type Bundle<-A: Type,-B: Type> is Type:
18 Bundle{first: A,second: B}
19# Read capability returning a detached Data value without component Access
20# wrapping. The supplied operation defines missing-value representation.
21type ValueRead<-H: Type,-V: Data> is Type:
22 ValueRead{get: H -> H & V}
23# Read/replace capability for a Data view V and potentially affine input C.
24# set consumes C and returns H; no automatic refusal receipt is added here.
25type ValueWrite<-H: Type,-C: Type,-V: Data> is Type:
26 ValueWrite{get: H -> H & V,set: H -> C -> H}
27# Publication capability consuming C and returning opaque H. The supplied
28# operation determines staging/refusal/ownership; this wrapper adds no rollback.
29type Send<-H: Type,-C: Type> is Type:
30 Send{send: H -> C -> H}
31# No-argument operation capability threading one affine opaque owner H.
32type Action<-H: Type> is Type:
33 Action{run: H -> H}
34# Operation capability consuming C and returning H plus detached Data V.
35# Use OwnedRequest when the result must itself retain affine owners.
36type Request<-H: Type,-C: Type,-V: Data> is Type:
37 Request{run: H -> C -> H & V}
38
39# Extract the first closed grant from a capability bundle, consuming it.
40def first(~A: Type,~B: Type,cap: Bundle<A,B>) -> A:
41 match cap:
42 case Bundle{a,_}: a
43# Extract the second closed grant from a capability bundle, consuming it.
44def second(~A: Type,~B: Type,cap: Bundle<A,B>) -> B:
45 match cap:
46 case Bundle{_,b}: b
47# Advanced setup projection extracting the closed operation from its grant.
48# Does not invoke it, access World or grant capabilities beyond that value.
49def read_field(~H: Type,~V: Data,cap: Read<H,V>) -> H -> H & Cmp.Access<V>:
50 match cap:
51 case Read{get}: get
52# Advanced setup projection extracting the closed operation from its grant.
53# Does not invoke it, access World or grant capabilities beyond that value.
54def write_read_field(~H: Type,~C: Type,~V: Data,cap: Write<H,C,V>) -> H -> H & Cmp.Access<V>:
55 match cap:
56 case Write{get,_}: get
57# Advanced setup projection extracting the closed operation from its grant.
58# Does not invoke it, access World or grant capabilities beyond that value.
59def write_field(~H: Type,~C: Type,~V: Data,cap: Write<H,C,V>) -> H -> C -> H:
60 match cap:
61 case Write{_,set}: set
62# Invoke a declared component read, returning the owner and Access<V>.
63# No extra validation is added beyond the bound get operation.
64def read(~H: Type,~V: Data,~cap: Read<H,V>,ctx: H) -> H & Cmp.Access<V>:
65 read_field(~H,~V,cap)(ctx)
66# Read the detached view through a write-capable component grant, returning
67# H and Access<V>. Does not consume or expose the stored affine C.
68def get(~H: Type,~C: Type,~V: Data,~cap: Write<H,C,V>,ctx: H) -> H & Cmp.Access<V>:
69 write_read_field(~H,~C,~V,cap)(ctx)
70# Invoke replacement with consumed C, returning the opaque owner. Refusal
71# results are determined by the bound operation; rejected C is not returned
72# by this signature. Canonical grants record errors for enclosing execution.
73def set(~H: Type,~C: Type,~V: Data,~cap: Write<H,C,V>,ctx: H,value: C) -> H:
74 write_field(~H,~C,~V,cap)(ctx,value)
75
76# Advanced setup projection extracting the closed operation from its grant.
77# Does not invoke it, access World or grant capabilities beyond that value.
78def value_read_field(~H: Type,~V: Data,cap: ValueRead<H,V>) -> H -> H & V:
79 match cap:
80 case ValueRead{get}: get
81# Advanced setup projection extracting the closed operation from its grant.
82# Does not invoke it, access World or grant capabilities beyond that value.
83def value_write_read_field(~H: Type,~C: Type,~V: Data,cap: ValueWrite<H,C,V>) -> H -> H & V:
84 match cap:
85 case ValueWrite{get,_}: get
86# Advanced setup projection extracting the closed operation from its grant.
87# Does not invoke it, access World or grant capabilities beyond that value.
88def value_write_field(~H: Type,~C: Type,~V: Data,cap: ValueWrite<H,C,V>) -> H -> C -> H:
89 match cap:
90 case ValueWrite{_,set}: set
91# Read detached V through ValueRead while returning its opaque owner.
92def value_read(~H: Type,~V: Data,~cap: ValueRead<H,V>,ctx: H) -> H & V:
93 value_read_field(~H,~V,cap)(ctx)
94# Read detached V through ValueWrite without replacing its stored value.
95def value_get(~H: Type,~C: Type,~V: Data,~cap: ValueWrite<H,C,V>,ctx: H) -> H & V:
96 value_write_read_field(~H,~C,~V,cap)(ctx)
97# Consume replacement C through ValueWrite and return the opaque owner.
98# The bound setter defines transaction/refusal behavior; this adds no receipt.
99def value_set(~H: Type,~C: Type,~V: Data,~cap: ValueWrite<H,C,V>,ctx: H,value: C) -> H:
100 value_write_field(~H,~C,~V,cap)(ctx,value)
101# Advanced setup projection extracting the closed operation from its grant.
102# Does not invoke it, access World or grant capabilities beyond that value.
103def send_field(~H: Type,~C: Type,cap: Send<H,C>) -> H -> C -> H:
104 match cap:
105 case Send{send}: send
106# Consume input C through a declared send operation and return H.
107# Publication timing and failure behavior belong to the supplied operation.
108def send(~H: Type,~C: Type,~cap: Send<H,C>,ctx: H,value: C) -> H:
109 send_field(~H,~C,cap)(ctx,value)
110# Advanced setup projection extracting the closed operation from its grant.
111# Does not invoke it, access World or grant capabilities beyond that value.
112def action_field(~H: Type,cap: Action<H>) -> H -> H:
113 match cap:
114 case Action{run}: run
115# Execute a declared no-argument action, consuming and returning H once.
116def action(~H: Type,~cap: Action<H>,ctx: H) -> H:
117 action_field(~H,cap)(ctx)
118# Advanced setup projection extracting the closed operation from its grant.
119# Does not invoke it, access World or grant capabilities beyond that value.
120def request_field(~H: Type,~C: Type,~V: Data,cap: Request<H,C,V>) -> H -> C -> H & V:
121 match cap:
122 case Request{run}: run
123# Execute a request with consumed input C, returning H and Data result V.
124# This is not the affine-output variant; use owned_request for Type results.
125def request(~H: Type,~C: Type,~V: Data,~cap: Request<H,C,V>,ctx: H,value: C) -> H & V:
126 request_field(~H,~C,~V,cap)(ctx,value)
127
128# One executor for every caller-authored finite capability shape.
129# Invoke a reusable universally quantified body with Data arguments and
130# declared Ops(H). H remains opaque to the body; closed caps must implement
131# the intended operations. This dispatcher adds no transaction or World checks.
132def invoke(~Ops: Type -> Type,~A: Data,~U: Type,~body: @-H: Type -> @-caps: Ops(H) -> A -> H -> H & U,~H: Type,~caps: Ops(H),args: A,ctx: H) -> H & U:
133 body(H,caps,args,ctx)
134
135# Additive owned input/result capability; existing Data APIs are unchanged.
136# Operation consuming an affine Input and returning H with affine Output.
137# Operation-specific results can preserve refused payloads; the wrapper does
138# not invent recovery or change their ownership semantics.
139type OwnedRequest<-H:Type,-Input:Type,-Output:Type> is Type:
140 OwnedRequest{run:H -> Input -> H & Output}
141# Advanced setup projection extracting the closed operation from its grant.
142# Does not invoke it, access World or grant capabilities beyond that value.
143def owned_request_field(~H:Type,~Input:Type,~Output:Type,cap:OwnedRequest<H,Input,Output>) -> H -> Input -> H & Output:
144 match cap:
145 case OwnedRequest{run}: run
146# Execute with affine input and return H plus the operation's affine
147# result. Branch on that result to handle payload recovery or refusal.
148def owned_request(~H:Type,~Input:Type,~Output:Type,~cap:OwnedRequest<H,Input,Output>,ctx:H,input:Input) -> H & Output:
149 owned_request_field(~H,~Input,~Output,cap)(ctx,input)
150# Args and output are fixed before opaque H; no Data restriction on owners.
151# Invoke the universally quantified body with affine arguments/output.
152# The callback consumes/returns H and consumes A exactly according to its
153# signature; any error/recovery branches belong to its own output contract.
154def invoke_owned(~Ops:Type -> Type,~A:Type,~U:Type,~body:@-H:Type -> @-caps:Ops(H) -> A -> H -> H & U,~H:Type,~caps:Ops(H),args:A,ctx:H) -> H & U:
155 body(H,caps,args,ctx)