1	import Base
2	import ./world.bend as W
3	import ./system.bend as Sys
4	import ./transaction.bend as T
5	import ./owner_product.bend as Product
6	import ./ordinary_recovery_declaration.bend as D
7	import ./ordinary_recoverable_array_resource.bend as F
8	import ./recovery_journal.bend as Journal
9	# Affine invocation input pairing caller Args with the retained capture.
10	# Admission refusal returns both through the registered request protocol.
11	type Request<Args:Type,Capture:Type> is Type:Request{args:Args,capture:Capture}
12	# Semantic outcome plus retained Out, capture and typed recovery receipts.
13	# Body errors stay inside Reply so transport success does not discard owners.
14	# Only explicitly journaled recoverable operations participate in restoration.
15	type Reply<Capture:Type,Recovery:Type,Error:Data,Out:Type> is Type:Reply{outcome:T.Outcome<Error>,output:Out,capture:Capture,recovery:Recovery}
16	# Affine recoverable-system owner pairing actual Registry and capture.
17	# Metadata or a printable name cannot substitute for the live registration.
18	type Owner<Registry:Type,Capture:Type> is Type:Owner{registry:Registry,capture:Capture}
19	# Completed retains World, owner, semantic outcome, Out and recovery.
20	# RegistrationRejected returns original Args and owner without running body.
21	# TransportFailed retains only World and is unreachable through the canonical
22	# closed runner, which returns semantic errors in Reply.
23	type Run<World:Type,Owner:Type,Args:Type,Error:Data,Out:Type,Recovery:Type> is Type:
24	  Completed{world:World,owner:Owner,outcome:T.Outcome<Error>,output:Out,recovery:Recovery}
25	  RegistrationRejected{world:World,owner:Owner,args:Args}
26	  TransportFailed{world:World}
27	# Defined returns World and registered capture owner; DefinitionRejected
28	# returns World and initial capture, without invoking the body.
29	type Defined<World:Type,Owner:Type,Capture:Type> is Type:
30	  Defined{world:World,owner:Owner}
31	  DefinitionRejected{world:World,capture:Capture}
32	def finished(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),outcome:T.Outcome<Error>,output:Out,result:Product.Owner<W.World<S,C,R,E>,Capture> & Recovery) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Capture,Recovery,Error,Out>>:
33	  match result:
34	    case (Product.Owner{world,capture},recovery):Sys.Succeeded{world,Reply{outcome,output,capture,recovery}}
35	def completing(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),state:Product.Owner<W.World<S,C,R,E>,Capture>,journal:List<Journal.Action(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery)>,result:T.Outcome<Error> & Out) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Capture,Recovery,Error,Out>>:
36	  match result:
37	    case (+outcome,output):finished(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,outcome,output,Journal.finish(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,journal,F.succeeded(~Error,outcome),state,D.empty(~S,~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops,~builder,declaration)(Unit{})))
38	def returned(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),result:F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,Recovery> & (T.Outcome<Error> & Out)) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Capture,Recovery,Error,Out>>:
39	  match result:
40	    case (F.Frame{state,journal},result):completing(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,state,journal,result)
41	# Advanced recoverable runner over World/capture product and shared journal.
42	# Canonical declared inverses determine commit/rollback receipts; arbitrary
43	# external effects or undeclared mutations are not made reversible. Returns
44	# outer Succeeded with semantic outcome and actual owners in Reply.
45	def runner(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,C,R,E>,request:Request<Args,Capture>) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Reply<Capture,Recovery,Error,Out>>:
46	  match request:
47	    case Request{args,capture}:returned(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,body(F.Frame<Product.Owner<W.World<S,C,R,E>,Capture>,Recovery>,D.root_grant(~S,~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops,~builder),args,F.Frame{Product.Owner{world,capture},[]}))
48	# Advanced type alias for the matching Registry/capture owner.
49	# Does not create a registration or validate a World by itself.
50	def Owned(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out)) -> Type:Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>
51	def registered(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),capture:Capture,result:Sys.RegistrationResult<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>) -> Defined<W.World<S,C,R,E>,Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,Capture>:
52	  match result:
53	    case Sys.Registered{world,registry}:Defined{world,Owner{registry,capture}}
54	    case Sys.RegistrationFailed{world}:DefinitionRejected{world,capture}
55	# Register a recoverable body with access derived from its declaration.
56	# Consumes capture on success; definition refusal returns it with World.
57	# No body or inverse operation runs at registration.
58	# Contract and consumers: docs/parity/recovery.md.
59	def define(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),world:W.World<S,C,R,E>,name:String,capture:Capture) -> Defined<W.World<S,C,R,E>,Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,Capture>:
60	  registered(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,capture,Sys.register(~S,~C,~R,~E,~Request<Args,Capture>,~Unit,~Reply<Capture,Recovery,Error,Out>,~runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body),world,name,D.access(~S,~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops,~builder,declaration)))
61	# Completion retains the Registry already advanced to its captured run tick.
62	# Semantic failure still returns its explicit Reply and recovery owners.
63	def done(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),outcome:T.Outcome<Error>,output:Out,capture:Capture,recovery:Recovery,result:W.World<S,C,R,E> & Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>) -> Run<W.World<S,C,R,E>,Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,Args,Error,Out,Recovery>:
64	  match result:
65	    case (world,registry):Completed{world,Owner{registry,capture},outcome,output,recovery}
66	def completed(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),result:Sys.RunResult<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>) -> Run<W.World<S,C,R,E>,Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,Args,Error,Out,Recovery>:
67	  match result:
68	    case Sys.RegistrationRejected{registry,world,Request{args,capture}}:RegistrationRejected{world,Owner{registry,capture},args}
69	    case Sys.Completed{registry,Sys.Succeeded{world,Reply{+outcome,output,capture,recovery}}}:done(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,outcome,output,capture,recovery,(world,registry))
70	    # Unreachable through the closed runner, which retains semantic errors in Reply.
71	    case Sys.Completed{_,Sys.Failed{world,_}}:TransportFailed{world}
72	# Validate registration and execute with retained capture and affine Args.
73	# Admission refusal returns original owners/Args. Completed returns semantic
74	# outcome, Out and typed recovery on both body success and failure; inspect
75	# outcome instead of assuming outer transport means commit. Every admitted completion consumes its captured lifecycle tick,
76	# including semantic failure; recovery ownership remains in Reply.
77	def run(~S:Data,~C:Type,~R:Type,~E:Data,~Capture:Type,~Recovery:Type,~Ops:Type -> Type,~Args:Type,~Error:Data,~Out:Type,~builder:D.Builder(~Product.Owner<W.World<S,C,R,E>,Capture>,~Recovery,~Ops),~declaration:D.Declaration<S,Product.Owner<W.World<S,C,R,E>,Capture>,Recovery,Ops,builder>,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & (T.Outcome<Error> & Out),owner:Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,world:W.World<S,C,R,E>,args:Args) -> Run<W.World<S,C,R,E>,Owner<Sys.Registry<S,C,R,E,Request<Args,Capture>,Unit,Reply<Capture,Recovery,Error,Out>,runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body)>,Capture>,Args,Error,Out,Recovery>:
78	  match owner:
79	    case Owner{registry,capture}:completed(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body,Sys.run(~S,~C,~R,~E,~Request<Args,Capture>,~Unit,~Reply<Capture,Recovery,Error,Out>,~runner(~S,~C,~R,~E,~Capture,~Recovery,~Ops,~Args,~Error,~Out,~builder,~declaration,~body),registry,world,Request{args,capture}))