diff --git a/app/spec/worker_coordination/worker_api.mli b/app/spec/worker_coordination/worker_api.mli index 87b8cc6..c53e996 100644 --- a/app/spec/worker_coordination/worker_api.mli +++ b/app/spec/worker_coordination/worker_api.mli @@ -1,7 +1,20 @@ -(** App/Worker coordination boundary. Pure data belongs to [Worker_pure_data]; - sealed authority is issued by the trusted - Worker runner. Abstraction is not authentication: every message, continuation, - receipt and resource is validated against its actual channel and owner. *) +(** {1 TLDR} + + Define the typed App/Worker boundary: read DTOs, durable intent, observations, + resource leases and host handoff capabilities. The trusted runner issues + sealed authority; [Worker_pure_coordinator.request] plans execution and + [Worker_effect_runner.submit] interprets it. This module itself performs no + transport I/O. Abstraction is not authentication: runtime checks still bind + every message, continuation, receipt and lease to its real channel and owner. + Queue admission, durable commitment and presentation confirmation are separate. + + The query/request GADTs depend on the capability families below. Their actual + public shapes include [Query (budget, query)], [Observe (budget, query)], + [Mutate intent], [Confirm (presentation, receipt)] and [Release observation]. + Replies distinguish [Not_admitted], [Answered] and [Interrupted]; interruption + after admission does not prove rollback. Sessions survive resident focus + changes but close/reopen, rebinding and account changes revoke execution. *) + module Graph = Logseq_db_types.Graph_types module Uuid = Graph.Uuid @@ -19,6 +32,44 @@ val equal_binding : binding -> binding -> bool type session = Worker_effect_authority.session type presentation = Worker_effect_authority.presentation +(** Sessions survive focus changes while resident. Close/reopen, account changes, + removal and rebinding revoke execution authority. Presentation has a separate + lifetime. Admission and completion recheck all identities, not just UUID. *) +type error = Worker_effect_authority.error = + | Revoked_session + | Invalid_input of string + | Response_budget_exceeded + | Stale_read of string + | Resync_required of string + | Host_change_in_progress + | Protocol_mismatch of string + | Db_error of Logseq_db_worker.Error.t + | Service_failed of string + | Unsupported_operation of string + +(** {1 Minimal usage example} + + The caller supplies a coordinator [state], a [session] obtained from a Ready + projection's Open resident, a typed [query], and the runner's [interpret]. + This example returns its ticket so the caller can later consume the reply: + {[ + match read_budget session ~maximum_items:1 ~maximum_bytes:4096 with + | Error error -> Error error + | Ok budget -> + match Worker_pure_coordinator.request !state session (Query (budget, query)) with + | Error error -> Error error + | Ok (ticket, transition) -> + state := transition.next; + List.iter interpret transition.instructions; + Ok ticket + ]} + [interpret] queues completion events for later serialized turns. Inspect + [Worker_pure_coordinator.reply] for admission, operation and interruption + outcomes, then feed [Forget ticket] through that coordinator. An observation + or file lease additionally requires its actual release acknowledgement. *) + +(** {1 Construction and validation} *) + val account_generation : session -> account_generation val graph_generation : session -> graph_generation val presentation_generation : presentation -> presentation_generation @@ -36,21 +87,6 @@ val worker_incarnation -> worker_generation:Journal_worker_ids.Worker.generation -> worker_incarnation -(** Sessions survive focus changes while resident. Close/reopen, account changes, - removal and rebinding revoke execution authority. Presentation has a separate - lifetime. Admission and completion recheck all identities, not just UUID. *) -type error = Worker_effect_authority.error = - | Revoked_session - | Invalid_input of string - | Response_budget_exceeded - | Stale_read of string - | Resync_required of string - | Host_change_in_progress - | Protocol_mismatch of string - | Db_error of Logseq_db_worker.Error.t - | Service_failed of string - | Unsupported_operation of string - type request_id = Worker_effect_authority.request_id val request_id : Uuid.t -> request_id @@ -83,6 +119,8 @@ type journal_day = Worker_effect_authority.journal_day val journal_day : int -> (journal_day, error) result +(** {1 Capability details} *) + type page = Worker_effect_authority.page type block = Worker_effect_authority.block @@ -282,6 +320,8 @@ val change_ack_session : change_ack -> session val change_ack_generation : change_ack -> string val change_ack_through : change_ack -> string +(** {2 Durable mutations} *) + type append_intent = Worker_effect_authority.append_intent (** Persist the complete bounded root/child/status payload and normalized stable @@ -357,7 +397,6 @@ val durable_intent_id : durable_intent -> Uuid.t val encode_durable_intent : durable_intent -> bytes val restore_durable_intent : session -> bytes -> (durable_intent, error) result - (** General mutations preserve today's exact preconditions and mutation IDs. Restores validate logical origin/account/graph and all bytes, allowing fresh execution sessions only for the same logical graph. Same ID/different payload @@ -458,6 +497,8 @@ type 'a reply = 'a Worker_effect_authority.reply = non-commit evidence cannot become Rejected. Replay must be durable/idempotent across restart, not merely a process-local duplicate cache. *) +(** {2 Observations and change windows} *) + type changefeed_notice = Worker_effect_authority.changefeed_notice = private { notice_session : session ; notice : Worker_pure_data.changefeed_signal @@ -509,6 +550,8 @@ type observation_notice = Worker_effect_authority.observation_notice = private } | Observations_resync of binding +(** {2 Assets and import sources} *) + type asset_consumer = Worker_effect_authority.asset_consumer type asset_demand = Worker_effect_authority.asset_demand type asset_file = Worker_effect_authority.asset_file @@ -619,6 +662,8 @@ val upload_operation : asset_notice -> upload_operation option replaces an underlying successful resource result and App never receives the handle. App-only late-reply cleanup cannot prove this; backend acquisition/ import ledger or atomic rollback must settle every Accepted operation. *) +(** {2 Typed execution requests} *) + type 'a request = 'a Worker_effect_authority.request = | Query : read_budget * 'a query -> 'a request | Observe : read_budget * 'a query -> 'a observed request @@ -658,6 +703,8 @@ type 'a request = 'a Worker_effect_authority.request = fail before enqueue, without a fabricated receipt/registration/lease ACK. *) val validate_request : session -> 'a request -> (unit, error) result +(** {1 Lifecycle and recovery} *) + type observation_update = Worker_effect_authority.observation_update = Update : 'a observed -> observation_update type projection_version = Worker_effect_authority.projection_version @@ -748,6 +795,8 @@ type bootstrap_state = Worker_effect_authority.bootstrap_state = state. The host must perform a handoff before retiring a graph/account/client; focus alone revokes presentation, not resident execution. The authoritative projection, not optimistic UI flags, admits the next session. *) +(** {2 Host handoff} *) + type host_change = Worker_effect_authority.host_change = | Account_will_change | Graph_will_close of Uuid.t @@ -816,6 +865,5 @@ type handoff_state = Worker_effect_authority.handoff_state = and removal uses the bound existing deletion owner. Do not dispatch a second legacy Close/Delete after that ACK. Auth/UI/client lifecycle stay with host. *) -(** Connection-bound validation used inside the direct effect runner. Methods below - map concrete Service messages, not fictional bytes or a separate adapter. The - factory is trusted integration, not proof of an honest backend. *) +(** Connection-bound validation remains the direct effect runner's responsibility. + The trusted integration is not itself proof of an honest backend. *) diff --git a/app/spec/worker_coordination/worker_effect_runner.mli b/app/spec/worker_coordination/worker_effect_runner.mli index 0d99b04..e3ad1c3 100644 --- a/app/spec/worker_coordination/worker_effect_runner.mli +++ b/app/spec/worker_coordination/worker_effect_runner.mli @@ -1,9 +1,40 @@ -(** Direct interpreter against the existing dbworker Service/client. No adapter, - second Worker client is introduced; the host selects its implementation explicitly. *) +(** {1 TLDR} + + Interpret the coordinator's private instructions through the existing Worker + client and its single host pump. {!create} borrows that client/account and + queues binding/bootstrap events; success does not imply Ready. {!submit} + performs scoped I/O, while {!on_event} routes actual mailbox completions. + The host owns serialization, UI/business state and shared client lifetime. + {!shutdown} returns [Draining], [Stopped] or [Shutdown_failed]; only [Stopped] + proves this runner's cleanup has reached its terminal fence. *) + module Worker = Worker_api type client = (Logseq_db_worker_lui.Logseq_db_worker_lui_service.request, Logseq_db_worker_lui.Logseq_db_worker_lui_service.response, Logseq_db_worker_lui.Logseq_db_worker_lui_service.push) Logseq_db_worker_lui.Journal_worker.client type t +type disposition = Consumed | Unowned_response | Broadcast | Dropped_envelope +type delivery = private { disposition : disposition; error : Worker.error option } + +type shutdown_state = Draining | Stopped | Shutdown_failed of Worker.error + +(** {1 Minimal usage example} + + The caller supplies the existing [client], verified [managed_origin]/[user_id], + [post] that queues serialized coordinator events, and the host's [publish]: + {[ + match create ~client ~managed_origin ~user_id ~post ~publish with + | Error error -> Error error + | Ok runner -> Ok runner + ]} + Keep the returned runner in the host. For each coordinator transition install + [next] first, then [List.iter (submit runner) transition.instructions]. Route + the existing pump through [on_event] before legacy dispatch and honor its + [disposition]. During retirement keep delivering real cleanup events and call + [shutdown runner] after progress until [Stopped]; retain failures for retry. + Closing the shared client also waits for every other owner. *) + +(** {1 Construction and validation} *) + val create : client:client -> managed_origin:string -> user_id:string -> post:(Worker_pure_coordinator.event -> unit) @@ -23,8 +54,8 @@ val create turns; publish does not own UI/business state. Ready comes only from the correlated registered Service baseline, never from independent legacy pushes. *) -type disposition = Consumed | Unowned_response | Broadcast | Dropped_envelope -type delivery = private { disposition : disposition; error : Worker.error option } +(** {1 Capability details} *) + val on_event : t -> (Logseq_db_worker_lui.Logseq_db_worker_lui_service.response, Logseq_db_worker_lui.Logseq_db_worker_lui_service.push) Logseq_db_worker_lui.Journal_worker.event -> delivery (** One shared host router calls this BEFORE legacy response dispatch. Ownership @@ -82,7 +113,8 @@ val submit : t -> Worker_pure_coordinator.instruction -> unit UI/auth/client continuation. Unknown outcomes retain their original permission and cleanup owner; they are never replayed with a fresh receipt. *) -type shutdown_state = Draining | Stopped | Shutdown_failed of Worker.error +(** {1 Lifecycle and recovery} *) + val shutdown : t -> shutdown_state (** Nonblocking and idempotent. Revoke ordinary admission, cancel/reconcile owned diff --git a/app/spec/worker_coordination/worker_pure_coordinator.mli b/app/spec/worker_coordination/worker_pure_coordinator.mli index c4233a5..d645a61 100644 --- a/app/spec/worker_coordination/worker_pure_coordinator.mli +++ b/app/spec/worker_coordination/worker_pure_coordinator.mli @@ -1,6 +1,23 @@ -(** Pure Worker request/observation/resource coordination, not the whole App. - Navigation/feed/Favorites algorithms, Capture editing and media UI stay with - their current business owners. step performs no DB/network/clock/callback IO. *) +(** {1 TLDR} + + Coordinate App requests, observations and resource ownership for one Worker + binding. The caller owns {!t}; {!step} and {!request} perform no I/O or + persistence. Each returns a private {!transition}: install [next] before + interpreting [instructions] in order. The runner queues later typed events. + Queue admission, durable outcomes and presentation confirmation are separate; + cancellation does not prove rollback. {!shutdown_state} reaches [Stopped] + only after real cleanup acknowledgements, not merely [Shutdown_requested]. + + The indexed event/instruction families depend on the capabilities below. + These are excerpts of the actual entry points, not additional APIs: + {[ + val initial : client_id:Worker.Uuid.t -> t + val step : t -> event -> transition + val request : t -> Worker.session -> 'a Worker.request + -> ('a ticket * transition, Worker.error) result + val reply : view -> 'a ticket -> 'a Worker.reply option + ]} *) + module Worker = Worker_api type t @@ -13,6 +30,27 @@ val view : t -> view val bootstrap : view -> Worker.bootstrap_state val projection : view -> Worker.projection option +(** {1 Minimal usage example} + + The caller supplies a coordinator [state] that has installed its real binding + and Ready bootstrap projection, an Open resident [session], validated [budget] + and [query], and the runner's [interpret]: + {[ + let apply transition = + state := transition.next; + List.iter interpret transition.instructions + in + match request !state session (Worker.Query (budget, query)) with + | Error error -> Error error + | Ok (ticket, transition) -> apply transition; Ok ticket + ]} + The host establishes [state] by applying the real [Worker_bound] and bootstrap + events through [step] before this flow. [interpret] queues all callbacks for + later serialized turns. Read [reply (view !state) ticket] after + completion; feed [Forget ticket] once its result has been consumed. *) + +(** {1 Capability details} *) + (** Latest original notifications accepted by Core for current residents since the previous view. Stale/foreign notices never reach this outlet; it retains no delivery history. Queued consumers still validate the notice session. *) @@ -98,6 +136,8 @@ val change_application_ready : view -> Worker.change_batch -> bool val change_application_error : view -> Worker.change_batch -> Worker.error option val equal_view : view -> view -> bool +(** {1 Lifecycle and recovery} *) + type shutdown_state = | Active | Draining @@ -181,6 +221,8 @@ type event = (* Return means no presentation consumer retains the capability. It is not an I/O ACK: failed/in-flight cleanup and metadata finalization stay owned until their matching real completions. Cleanup retries remain possible while owned. *) +(** {2 Cleanup instructions} *) + (** Cleanup identity allocated by Core before sending a replacement. It records an obligation, not successful registration. Runner may inspect it but cannot construct or retarget it; cancellation can clean up even if no handle arrived. *) @@ -257,6 +299,8 @@ val request -> 'a Worker.request -> ('a ticket * transition, Worker.error) result +(** {2 Mutation reconciliation} *) + type mutation_reconciliation = | Submission_ticket of Worker.submission_outcome ticket | Confirmation_ticket of Worker.confirmation ticket @@ -280,6 +324,8 @@ val settle_applied_mutation : t -> presentation:Worker.presentation -> applied_presentation:Worker.presentation -> Worker.durable_intent -> (mutation_settlement * transition, Worker.error) result +(** {2 Applying change windows} *) + (** Start application of an actually delivered batch. An active successful attempt cannot be replaced by a duplicate pull; an explicit retry after a failure gets a new token. The root itself is applied only after its UI state. *) diff --git a/app/spec/worker_coordination/worker_pure_data.mli b/app/spec/worker_coordination/worker_pure_data.mli index cebd0c8..716deac 100644 --- a/app/spec/worker_coordination/worker_pure_data.mli +++ b/app/spec/worker_coordination/worker_pure_data.mli @@ -1,7 +1,41 @@ -(** Pure query values shared by the coordinator and Worker. Constructor tags - preserve the canonical JSON identity of persisted mutation payloads. *) +(** {1 TLDR} + + Define pure query DTOs shared by the App coordinator and Worker. + Constructor tags preserve canonical JSON identity for persisted mutation + payloads; this module performs no I/O and grants no execution authority. + The mutually recursive data family below includes revision preconditions, + explicit present/missing lookups, bounded page members and change windows. + {!valid_append_node} validates append trees; requests execute through + [Worker_api.Query] and [Worker_pure_coordinator.request], not through DTOs. *) + open Logseq_db_types.Graph_types +type changefeed_signal = + | Changes_available of { generation : string; through : string } + | Resync_required of { generation : string; reason : string } + +(** {1 Minimal usage example} + + The caller supplies a [session], a [budget] validated by [Worker_api.read_budget], + the coordinator [state] and the runner's [interpret]. This read consumes the + DTOs through their public owner: + {[ + match Worker_pure_coordinator.request !state session + (Worker_api.Query (budget, Worker_api.Admission)) with + | Error error -> Error error + | Ok (ticket, transition) -> + state := transition.next; + List.iter interpret transition.instructions; + Ok ticket + ]} + [interpret] queues completion events for later serialized turns. The caller + reads the eventual typed reply through [Worker_pure_coordinator.reply]. *) + +(** {1 Construction and validation} + + These bounds are part of request, response and tree validation. A valid + DTO alone does not prove that its session, revisions or budgets are current. *) + val maximum_request_bytes : int val maximum_response_bytes : int val maximum_push_bytes : int @@ -15,6 +49,12 @@ val maximum_changed_uuids : int val maximum_property_values : int val maximum_filter_values : int +(** {1 Capability details} + + This recursive family is kept together to preserve its generated JSON + representation. Lookups distinguish missing records from an empty page; + version strings and preconditions must be passed back to their owning API. *) + type precondition_scope = V2_children_scope of Uuid.t and task_status = Uuid.t @@ -144,8 +184,6 @@ and admission_inspection = } [@@deriving yojson] -type changefeed_signal = - | Changes_available of { generation : string; through : string } - | Resync_required of { generation : string; reason : string } +(** {1 Observation and helpers} *) val valid_append_node : append_node -> bool diff --git a/logseq_db_worker/spec/effect_runner/effect_runner.mli b/logseq_db_worker/spec/effect_runner/effect_runner.mli index 5d54300..1d88bd1 100644 --- a/logseq_db_worker/spec/effect_runner/effect_runner.mli +++ b/logseq_db_worker/spec/effect_runner/effect_runner.mli @@ -1,4 +1,23 @@ -(** Eio interpreter for Worker requests and typed overlay transitions. *) +(** {1 TLDR} + + Interpret Worker instructions and typed overlay transitions with Eio. + The serial reducer owns policy and state; {!create} supplies an I/O runner, + and {!submit} executes its instructions and posts later typed completion + events. Database attachments, observations, file retains and cleanup ledgers + remain owned until their real release/join acknowledgements. Admission or + cancellation alone is not cleanup, rollback or host action permission. + + Dependencies and typed callback inputs appear below. Primary excerpts: + {[ + val create : sw:Eio.Switch.t -> dependencies + -> post:(Logseq_db_worker_pure_reducer.Core.event -> unit) + -> recovery_current:(Logseq_db_worker_pure_reducer.Core.upload_recovery_ticket -> bool) + -> upload_current:(Logseq_db_worker_pure_reducer.Asset_upload.ticket -> bool) + -> asset_current:(Logseq_sync_pure_reducer.Asset_transfer.ticket -> bool) + -> (t, create_error) result + val submit : t -> Logseq_db_worker_pure_reducer.Core.instruction -> unit + val shutdown : t -> unit + ]} *) type t type runtime @@ -6,9 +25,35 @@ type sync_runner type dependencies type dependency_error = Invalid_dependency of string type create_error = Invalid_create of string + +(** {1 Minimal usage example} + + The caller supplies [sw], validated [dependencies], a reducer-produced + [instruction], a serialized event-queue [post], and predicates reading the + installed reducer state: + {[ + match create ~sw dependencies ~post ~recovery_current ~upload_current ~asset_current with + | Error error -> Error error + | Ok runner -> + Fun.protect + ~finally:(fun () -> shutdown runner) + (fun () -> + submit runner instruction; + run_until_retired runner; + Ok ()) + ]} + [run_until_retired] is the caller's loop, not a runner method. It preserves + pump/callback delivery and the enclosing switch until actual scoped writer, + listener, resource and Sync barriers finish. [submit] does not return their + results; checked cleanup failures retain their original owner for retry. *) + +(** {1 Construction and validation} *) + type id_token_request type id_token_cache +(** {2 Identity-token exchange} *) + val id_token_request_id : id_token_request -> string val id_token_cache @@ -34,6 +79,8 @@ val invalidate_id_token val reconcile_authenticated_user : id_token_cache -> user_id:string option -> unit val shutdown_id_token_cache : id_token_cache -> unit +(** {2 Runner dependencies} *) + val runtime : fork:(sw:Eio.Switch.t -> (unit -> unit) -> unit) -> sleep:(float -> unit) @@ -63,6 +110,8 @@ val create -> asset_current:(Logseq_sync_pure_reducer.Asset_transfer.ticket -> bool) -> (t, create_error) result +(** {1 Capability details} *) + val submit : t -> Logseq_db_worker_pure_reducer.Core.instruction -> unit (** Accept a bounded diagnostic only for its live scoped asset request. The @@ -82,7 +131,7 @@ val await_reply -> post:(unit -> unit) -> Worker_pure_read.answer -val shutdown : t -> unit +(** {2 Assets and durable mutations} *) val retain_asset_file : t @@ -159,6 +208,8 @@ val acknowledge_mutation : t -> scope:Logseq_sync_pure_reducer.Core.graph_scope -> intent:Logseq_db_worker_contract.Worker_pure_mutation.durable_intent -> original:(string * string * string) option -> current:(unit -> bool) -> (unit,string) result +(** {2 Observations and changefeed} *) + (** Actual paused-listener/predecessor-snapshot registration on the existing DB. A sampled typed error remains registered and can recover on the next invalidation/Refresh; only allocation or activation failure aborts registration. @@ -220,6 +271,8 @@ val acknowledge_change_batch : t -> registration:int64 -> scope:Logseq_sync_pure val retire_changefeed : t -> registration:int64 -> unit +(** {1 Lifecycle and recovery} *) + (** Permanently stop new physical graph-operation admission for this incarnation, join already reserved protected tasks even if Service waiters canceled, then join their actual serial reducer callback barrier. This is only writer evidence; @@ -258,6 +311,8 @@ val bind_host_copy:t -> handoff_id:Logseq_db_types.Graph_types.Uuid.t -> Logseq_sync_pure_reducer.Core.mirror_deletion -> (unit,Logseq_db_worker_pure_reducer.Core.effect_error)result val release_host_copy:t -> registration:int64 -> (unit,string)result +(** {2 Import source recovery} *) + (** Read-only complete source recovery: missing store is known empty; no schema, staging, acquisition or execution is performed. Cursor pages obey both item and canonical encoded byte budgets. Every proof rechecks its logical owner. *) @@ -273,3 +328,8 @@ val confirm_import_input:t -> scope:Logseq_sync_pure_reducer.Core.graph_scope evidence, under the existing writer fence. Complete bytes and proof remain. *) val acknowledge_import_input:t -> scope:Logseq_sync_pure_reducer.Core.graph_scope -> input:string -> prepared:string -> current:(unit -> bool) -> (unit,string)result + +(** Stop this runner and its delegated Sync runner. Actual scoped cleanup and + callback barriers above remain the lifecycle owner's obligation; a unit + return is not a checked release or permission to discard an unsettled owner. *) +val shutdown : t -> unit diff --git a/logseq_db_worker/spec/pure_reducer/asset_upload.mli b/logseq_db_worker/spec/pure_reducer/asset_upload.mli index c1472e8..746a2cf 100644 --- a/logseq_db_worker/spec/pure_reducer/asset_upload.mli +++ b/logseq_db_worker/spec/pure_reducer/asset_upload.mli @@ -1,8 +1,45 @@ -(** One durable explicit import, owned by the worker and independent of download demand. *) +(** {1 TLDR} + + Coordinate one explicit durable import independently of download demand. + The caller owns {!t}; {!step} is pure and returns next state plus ordered + {!instruction}s. The worker interpreter owns persistence, upload and staging + release. {!checkpoint} exposes the last durable intent for recovery; + cancellation requests cleanup and does not prove upload rollback. + + The dependent variants are defined below. Actual entry-point excerpts: + {[ + val create : scope:Scope.graph_scope -> available:bool -> t + val step : t -> event -> t * instruction list + val checkpoint : t -> Intent.t option + val status : t -> status option + ]} *) + module Intent = Logseq_db_types.Asset_upload_intent module Scope = Logseq_sync_pure_reducer.Core +type t + +(** [available] admits PUT work only when foreground networking and the graph key + are available. Local durability and cancellation remain active while paused. *) +val create : scope:Scope.graph_scope -> available:bool -> t + +(** {1 Minimal usage example} + + The caller supplies the current [scope], network/key [available] flag, an + already validated upload [intent] and the worker's [interpret]: + {[ + let state = ref (create ~scope ~available) in + let next, instructions = step !state (Start intent) in + state := next; + List.iter interpret instructions + ]} + [interpret] queues exact [Completed (ticket, completion)] events for later + serialized turns. After restart, use [Restore intent] with stored durable + evidence instead of creating a new operation identity. *) + +(** {1 Capability details} *) + type failure = | Network | Authentication @@ -22,6 +59,14 @@ type status = | Cancelled | Failed_upload of failure +(** {1 Lifecycle and recovery} + + The reducer issues each ticket for an exact graph scope and import operation. + The runner holds it until completion; {!ticket_current} rejects retired or + superseded work. Tickets are process-local; the durable intent is the recovery + identity. [Retry] resumes retained work, and [Shutdown] cancels pending work + and stops the reducer without certifying physical cleanup or deleting intent. *) + type ticket = private { id : int ; scope : Scope.graph_scope @@ -62,12 +107,7 @@ type event = | Retry | Availability_changed of bool | Shutdown - -type t - -(** [available] admits PUT work only when foreground networking and the graph key - are available. Local durability and cancellation remain active while paused. *) -val create : scope:Scope.graph_scope -> available:bool -> t +(** {1 Observation and helpers} *) val checkpoint : t -> Intent.t option val failure : t -> failure option diff --git a/logseq_db_worker/spec/pure_reducer/core.mli b/logseq_db_worker/spec/pure_reducer/core.mli index fc58d61..6cf7f1e 100644 --- a/logseq_db_worker/spec/pure_reducer/core.mli +++ b/logseq_db_worker/spec/pure_reducer/core.mli @@ -1,4 +1,50 @@ -(** Pure Logseq DB worker lifecycle and request-routing policy. *) +(** {1 TLDR} + + Own pure DB Worker lifecycle and request routing, including graph state, + pending requests, Sync delegation and resource cleanup ledgers. The host owns + {!state}; {!initial} validates construction, and {!step} returns a {!transition} + with [next] and ordered [effects]. Install [next] before interpreting effects; + callbacks queue exact completion events for a later serialized turn. No DB, + network, clock or callback I/O occurs in this reducer. + + The runner GADT and dependent instruction/event families remain below. + These are accurate entry-point excerpts, not additional declarations: + {[ + val initial : config -> (state, create_error) result + val step : state -> event -> transition + val view : state -> view + ]} + Cleanup admission is not a physical ACK. Scope/attempt identity must still be + checked at runtime; process-local tickets do not replace durable intent. *) + +(** {1 Minimal usage example} + + The caller supplies validated [config] and the worker runner's [interpret]: + {[ + match initial config with + | Error error -> Error error + | Ok first -> + let state = ref first in + let transition = step !state Start in + state := transition.next; + List.iter interpret transition.effects; + Ok state + ]} + [interpret] queues real completions, preserving the original effect ticket. + The host applies later events with the same install-before-interpret order. + On retirement feed [Shutdown], then continue processing admitted cleanup and + callback barriers; the view's shutdown flag alone is not a physical join. *) + +(** {1 Construction and validation} *) + +type config + +val config + : worker:Logseq_db_worker_contract.Config.t + -> sync:Logseq_sync_pure_reducer.Core.config + -> config + +(** {1 Capability details} *) type graph_phase = | Graph_closed @@ -14,6 +60,8 @@ type graph_state = ; error : Logseq_db_worker_contract.Error.t option } +(** {2 Request and execution identities} *) + type request_id val request_id_of_int64 : int64 -> request_id @@ -96,6 +144,8 @@ type output = | Scoped_graph_push of Logseq_sync_pure_reducer.Core.graph_scope * Worker_pure_data.changefeed_signal | Diagnostic of string +(** {2 Upload recovery and instructions} *) + type upload_recovery_ticket = private { scope : Logseq_sync_pure_reducer.Core.graph_scope ; after : Logseq_db_types.Graph_types.Uuid.t option @@ -122,13 +172,6 @@ val instruction_diagnostic : instruction -> string val equal_instruction : instruction -> instruction -> bool val equal_instructions : instruction list -> instruction list -> bool -type config - -val config - : worker:Logseq_db_worker_contract.Config.t - -> sync:Logseq_sync_pure_reducer.Core.config - -> config - type view = { graph : graph_state ; sync : Logseq_sync_pure_reducer.Core.state @@ -214,6 +257,8 @@ type coordination_state = val coordination_state : state -> coordination_state val import_context_for_scope : state -> Logseq_sync_pure_reducer.Core.graph_scope -> Logseq_sync_pure_reducer.Core.asset_context option +(** {1 Lifecycle and recovery} *) + (** Pure admission/epoch/tombstone ownership for real query subscriptions. Physical listeners and snapshot leases remain with the effect owner. A released logical ID cannot allocate later if Cancel overtook registration. @@ -314,6 +359,8 @@ module Observation_registry : sig val retire_registration : t -> registration:int64 -> t end +(** {2 Changefeed ownership} *) + (** One registered changefeed consumer for one physical DB session. Registered replacements require actual prior retirement. An unapplied pull is retained verbatim until its exact ACK succeeds. *) @@ -362,6 +409,7 @@ module Changefeed_owner : sig val retire : t -> registration:int64 -> t end +(** {2 Orphan resource cleanup} *) (** Cleanup ownership transferred by the real Mailbox's exactly-once discarded success callback. Any unsettled physical release blocks new acquisition; @@ -445,6 +493,8 @@ module Registration_retirement : sig val released:t -> registration:int64 -> t end +(** {2 Host handoff} *) + (** Pure one-use host permission policy. External settlement inputs are supplied only after actual I/O/resource owners have acknowledged. This model itself performs no quiescence, callbacks, randomness, file inspection or deletion. *) @@ -489,5 +539,7 @@ module Host_handoff : sig val receipt_copy_generation:receipt -> Logseq_overlay_db.Types.mirror_generation option end +(** {1 Observation and helpers} *) + val host_fence_blocks : state -> Logseq_db_types.Graph_types.Uuid.t -> bool val host_fence_active : state -> Logseq_sync_pure_reducer.Core.host_fence option diff --git a/logseq_overlay_db/spec/database.mli b/logseq_overlay_db/spec/database.mli index 9b331ad..114b63a 100644 --- a/logseq_overlay_db/spec/database.mli +++ b/logseq_overlay_db/spec/database.mli @@ -1,38 +1,81 @@ -(** The lifecycle and transaction boundary of the logical Logseq database. +(** {1 TLDR} - A value of this module presents one coherent graph assembled from two durable - sources: the authoritative mirror and the ordered local outbox. Callers do not - choose between those sources. They inspect a mirror, open the logical database, - capture an immutable snapshot, and read the projection represented by that - snapshot. + Own the lifecycle and transaction boundary of one logical Logseq graph: + a coherent projection of the durable authoritative mirror and local outbox. + Inspect an available mirror, {!open_} it, acquire a {!snapshot}, read it, + {!release_snapshot}, then {!close} the database and check its result. + Writes are serialized durable operations; cryptography remains with the caller. + Snapshot activation owns cancelable staging resources. No raw database, + filesystem handle or outbox record crosses this boundary. *) - Writes commit in one serialized operation. Synchronization uses a preparation - only when external cryptography must occur between observation and durable - application. Snapshot activation remains explicitly cancelable because it owns - staged filesystem resources. +module Graph = Logseq_db_types.Graph_types + +type dependencies +type mirror_inspection + +type t +type snapshot + +(** [open_ ~sw dependencies inspection ~graph_name] validates the display name, + acquires exclusive ownership, and restores an available inspected mirror. + Resources are tied to [sw], but callers should still use [close] to observe + shutdown errors. *) +val open_ + : sw:Eio.Switch.t + -> dependencies + -> mirror_inspection + -> graph_name:string + -> (t, Types.open_error) result + +(** Closes storage and invalidates the database's outstanding snapshots and + subscriptions. *) +val close : t -> (unit, Types.close_error) result + +(** Captures the current coherent logical projection as a read lease. *) +val current_snapshot : t -> (snapshot, Types.read_error) result + +(** Returns the generation and projection revision captured by the snapshot. *) +val snapshot_version : snapshot -> Types.snapshot_version + +(** Prevents new reads from starting through [snapshot] and releases its pinned + roots after already-started reads finish. *) +val release_snapshot : snapshot -> unit - No Datascript database, entity id, filesystem handle, or outbox record crosses - this interface. +(** Reads graph identity, schema, admission facts, limits, and version from the + snapshot. *) +val graph_info : snapshot -> (Types.graph_info, Types.read_error) result - Examples use [require_ok] to keep attention on resource ownership and protocol - order. Production callers should preserve and handle the typed errors instead. +(** {1 Minimal usage example} + The caller supplies an Eio [sw], validated [dependencies], the support + directory, [graph_id] and [graph_name]. [require_ok] raises on a typed error + for this example; production callers should retain and handle those errors. {[ let require_ok = function | Ok value -> value | Error _ -> failwith "database operation failed" - ]} *) - -module Graph = Logseq_db_types.Graph_types + in + let inspection = + inspect_mirror ~application_support_directory ~graph_id |> require_ok + in + let database = open_ ~sw dependencies inspection ~graph_name |> require_ok in + Fun.protect + ~finally:(fun () -> close database |> require_ok) + (fun () -> + let snapshot = current_snapshot database |> require_ok in + Fun.protect + ~finally:(fun () -> release_snapshot snapshot) + (fun () -> graph_info snapshot |> require_ok)) + ]} + An absent mirror requires snapshot activation before opening. Detailed examples + below use the same caller-defined [require_ok] convention. *) -(** {1 Establishing the operating envelope} +(** {1 Construction and validation} Limits and dependencies are validated before any path is inspected or any resource is acquired. Keeping them immutable makes every later admission, batching, cursor, and clock decision part of the database's construction. *) -type dependencies - (** [dependencies] validates and fixes the clocks and public capability limits used by one database. Every bound must be positive, and a wire batch must fit within the outbox byte budget. *) @@ -45,15 +88,15 @@ val dependencies (** Immutable limits fixed by [dependencies], before any graph is opened. *) val dependency_limits : dependencies -> Types.capability_limits -(** {1 Discovering a durable mirror} +(** {1 Capability details} + + {2 Discovering a durable mirror} Opening begins with observation rather than mutation. An inspection records what was found at the graph's canonical database path. The recorded mirror generation prevents a stale observation from opening, deleting, or collecting a different mirror. *) -type mirror_inspection - (** [inspect_mirror ~application_support_directory ~graph_id] derives the canonical path and records whether the mirror is absent or available. An available inspection includes its graph identity, checkpoint, checksum, and generation. *) @@ -210,45 +253,13 @@ val collect_garbage : mirror_inspection -> (Types.garbage_collection, Types.garbage_collection_error) result -(** {1 Opening the logical database} +(** {2 Opening the logical database} An open database owns the mirror, the authoritative Datascript lineage, the queryable outbox, and the ordered change dispatcher. A snapshot is a leased, immutable pair of authoritative and outbox roots; every read through it sees that same pair even while later commits advance the open database. *) -type t -type snapshot - -(** [open_ ~sw dependencies inspection ~graph_name] validates the display name, - acquires exclusive ownership, and restores an available inspected mirror. - Resources are tied to [sw], but callers should still use [close] to observe - shutdown errors. *) -val open_ - : sw:Eio.Switch.t - -> dependencies - -> mirror_inspection - -> graph_name:string - -> (t, Types.open_error) result - -(** Closes storage and invalidates the database's outstanding snapshots and - subscriptions. *) -val close : t -> (unit, Types.close_error) result - -(** Captures the current coherent logical projection as a read lease. *) -val current_snapshot : t -> (snapshot, Types.read_error) result - -(** Returns the generation and projection revision captured by the snapshot. *) -val snapshot_version : snapshot -> Types.snapshot_version - -(** Prevents new reads from starting through [snapshot] and releases its pinned - roots after already-started reads finish. *) -val release_snapshot : snapshot -> unit - -(** Reads graph identity, schema, admission facts, limits, and version from the - snapshot. *) -val graph_info : snapshot -> (Types.graph_info, Types.read_error) result - (** Reports current outbox occupancy and the limits against which future local commits and submissions will be admitted. *) val inspect_admission @@ -346,7 +357,9 @@ val get_structure (fun () -> get_outline_blocks snapshot uuids) ]} *) -(** {1 Crossing from a snapshot to live changes} +(** {1 Lifecycle and recovery} + + {2 Crossing from a snapshot to live changes} Subscription registration and predecessor capture are one atomic operation. The returned subscription starts paused, so a consumer can hydrate from the @@ -395,7 +408,7 @@ val unlisten : subscription -> unit raise exn) ]} *) -(** {1 Committing optimistic local intent} +(** {2 Committing optimistic local intent} A local mutation is checked against equality tokens obtained from earlier logical reads. One serialized operation validates identity and preconditions, @@ -537,7 +550,7 @@ val discard_blocked |> require_ok ]} *) -(** {1 Handing cryptography to the caller} +(** {2 Handing cryptography to the caller} The database owns durable records and crypto item identities, while the sync layer owns encryption and decryption. Requests expose only bounded strings. @@ -554,7 +567,7 @@ val unprotection_ciphertexts : unprotection_request -> (Types.crypto_item_id * string) list -(** {1 Advancing synchronization} +(** {2 Advancing synchronization} Sync reads one opaque token and uses it as the compare-and-set boundary for either direction. Outbox transitions prepare client submissions and terminal @@ -674,6 +687,8 @@ val apply_authoritative apply_authoritative database preparation ~decrypted |> require_ok ]} *) +(** {1 Observation and helpers} *) + (** Reads validated metadata for explicit asset identities. Missing/non-asset identities are omitted; no binary IO occurs. At most 200 identities per call. *) val get_asset_descriptors diff --git a/logseq_overlay_db/spec/server_cursor.mli b/logseq_overlay_db/spec/server_cursor.mli index 5b6e3f0..df3bff4 100644 --- a/logseq_overlay_db/spec/server_cursor.mli +++ b/logseq_overlay_db/spec/server_cursor.mli @@ -1,8 +1,24 @@ -(** A non-negative authoritative server transaction cursor. *) +(** {1 TLDR} + + Represent a non-negative authoritative server transaction cursor without I/O. + Validate incoming integers with [of_int64]; [zero] is the initial baseline. *) type t = Logseq_db_types.Server_cursor.t val zero : t val of_int64 : int64 -> (t, [ `Negative_cursor ]) result val to_int64 : t -> int64 + +(** {1 Minimal usage example} + + The caller supplies the integer [wire_cursor]: + {[ + match of_int64 wire_cursor with + | Ok cursor -> Ok (to_int64 cursor) + | Error `Negative_cursor -> Error `Negative_cursor + ]} *) + +(** {1 Observation and helpers} + + Compare validated cursors without converting them back to integers. *) val equal : t -> t -> bool val compare : t -> t -> int diff --git a/logseq_overlay_db/spec/types.mli b/logseq_overlay_db/spec/types.mli index 72946ae..e2fdffd 100644 --- a/logseq_overlay_db/spec/types.mli +++ b/logseq_overlay_db/spec/types.mli @@ -1,4 +1,12 @@ -(** Stable UUID-addressed values for the logical Logseq overlay database. *) +(** {1 TLDR} + + Describe UUID-addressed logical overlay data, revision tokens and typed + operation outcomes without I/O or persistence. {!graph_info} identifies one + coherent projection; {!snapshot_version} binds its generation and revision. + Local intent, outbox transport and authoritative commits have separate result + types: local admission or commitment is not remote acceptance. + [Database] owns execution and durable resource lifecycles; tokens and records + here do not acquire a database, lease or current authority. *) module Graph = Logseq_db_types.Graph_types @@ -66,6 +74,21 @@ type graph_info = ; version : snapshot_version } +(** {1 Minimal usage example} + + The caller supplies an acquired [snapshot] and releases it through [Database] + after use. This function consumes a {!graph_info} returned by the actual owner: + {[ + let read_identity snapshot = + match Database.graph_info snapshot with + | Error error -> Error error + | Ok info -> Ok (info.graph_uuid, info.version) + ]} + The returned version describes that captured projection; it does not refresh + later reads or authorize a write without the owner's preconditions. *) + +(** {1 Capability details} *) + type admission_inspection = { active_records : int ; active_bytes : int @@ -234,6 +257,8 @@ type logical_change_summary = } | Logical_resync_required of resync_reason +(** {2 Local mutation intent and outcomes} *) + type block_tree = { uuid : Graph.block_uuid ; title : string @@ -339,6 +364,13 @@ val delete_conflict_kind_set val delete_conflict_kinds : delete_conflict_kind_set -> delete_conflict_kind list +(** {1 Lifecycle and recovery} + + Mutation fingerprints and receipts retain durable identity; transport attempts + and acceptance barriers describe different evidence. A stale/unknown attempt + cannot be treated as a proven rollback. The database validates owner, token + and generation at execution; deserializing an opaque token grants no authority. *) + type remote_won_reason = | Before_submission | Proven_unexecuted @@ -433,6 +465,8 @@ val remote_won_proof_earliest_conflict_cursor : remote_won_proof -> server_curso val remote_won_proof_operation : remote_won_proof -> outliner_operation val remote_won_proof_digest : remote_won_proof -> mutation_fingerprint +(** {2 Submission batches} *) + type submission_descriptor = { mutation_id : Graph.Uuid.t ; fingerprint : mutation_fingerprint @@ -569,6 +603,8 @@ type terminal_receipt = ; transport_disposition : terminal_transport_disposition } +(** {2 Authoritative history} *) + type authoritative_input_error = | Invalid_server_cursor | Invalid_encoded_transaction @@ -629,6 +665,12 @@ type authoritative_commit = ; logical_change_summary : logical_change_summary } +(** {1 Observation and helpers} + + Mirror observations and operation-specific errors are facts returned by their + execution owner. A recorded generation detects replacement; it does not keep + a resource live or turn a failed physical cleanup into an acknowledgement. *) + type mirror_presence = | Absent of { generation : mirror_generation } | Available of diff --git a/logseq_sync/spec/effect_runner/asset_cache.mli b/logseq_sync/spec/effect_runner/asset_cache.mli index 2809235..234c473 100644 --- a/logseq_sync/spec/effect_runner/asset_cache.mli +++ b/logseq_sync/spec/effect_runner/asset_cache.mli @@ -1,7 +1,30 @@ -(** Cache resources have no public execution interface. Business requests enter - [Core.step]; the resulting effect is submitted to [Effect_runner.submit]. *) +(** {1 TLDR} + + Name the opaque cache resources owned by the Sync effect runner. + There is no public cache constructor or execution API here: business requests + enter [Logseq_sync_pure_reducer.Core.step], and the runner performs cache I/O. + Cache handles and staged values are process-local resources, not durable proofs. *) + type t type handle type error type staged + +(** {1 Minimal usage example} + + The caller supplies a current reducer [state], an [event], and the actual + [runner]. This is the public execution path, not direct cache access: + {[ + let transition = Logseq_sync_pure_reducer.Core.step !state event in + state := transition.next; + List.iter + (function + | Logseq_sync_pure_reducer.Core.Run runner_effect -> + Effect_runner.submit runner runner_effect + | instruction -> interpret_other instruction) + transition.effects + ]} + The caller supplies [interpret_other] for delegated work and publications. + Runner callbacks queue events for a later serialized reducer turn; the runner + owns cache cleanup and is shut down by its lifecycle owner. *) diff --git a/logseq_sync/spec/effect_runner/asset_codec.mli b/logseq_sync/spec/effect_runner/asset_codec.mli index d5e1b9e..7a9b626 100644 --- a/logseq_sync/spec/effect_runner/asset_codec.mli +++ b/logseq_sync/spec/effect_runner/asset_codec.mli @@ -1,11 +1,16 @@ -(** The asset envelope encrypts raw file bytes, not a Transit title value. *) +(** {1 TLDR} + + Encode and verify bounded asset file bytes, using caller-supplied crypto. + [encode] returns wire bytes or an error; [decode] alone creates {!verified} + plaintext bound to the expected asset version. No file I/O or persistence + occurs here. Envelopes encrypt raw file bytes, not Transit title values. + An envelope failure must never fall back to raw bytes. *) + type crypto = { encrypt : key:string -> plaintext:string -> (string * string, string) result ; decrypt : key:string -> iv:string -> ciphertext:string -> (string, string) result } -val checksum : string -> string - val encode : maximum_plaintext_bytes:int -> crypto:crypto @@ -22,8 +27,6 @@ type decode_error = | Decryption_failed of string | Checksum_mismatch -val decode_error_message : decode_error -> string - (** Only a successful bounded decode creates this value. It binds plaintext to the expected version; there is no unchecked bytes-to-verified constructor. *) type verified @@ -39,3 +42,20 @@ val decode -> expected:Logseq_db_types.Asset_descriptor.version -> string -> (verified, decode_error) result + +(** {1 Minimal usage example} + + The caller supplies [crypto], [key], [expected], [wire] and a positive + [maximum_plaintext_bytes] matching its resource budget: + {[ + match decode ~maximum_plaintext_bytes ~crypto ~key ~expected wire with + | Ok verified -> Ok (verified_version verified, verified_bytes verified) + | Error error -> Error (decode_error_message error) + ]} + Verification failure leaves the caller responsible for rejecting the input; + no cache handle or file is acquired by this operation. *) + +(** {1 Observation and helpers} *) + +val checksum : string -> string +val decode_error_message : decode_error -> string diff --git a/logseq_sync/spec/effect_runner/effect_runner.mli b/logseq_sync/spec/effect_runner/effect_runner.mli index 9c59b9c..2a4f853 100644 --- a/logseq_sync/spec/effect_runner/effect_runner.mli +++ b/logseq_sync/spec/effect_runner/effect_runner.mli @@ -1,8 +1,50 @@ -(** Eio-native interpreter for [Logseq_sync_pure_reducer.Core.runner_effect]. *) +(** {1 TLDR} + + Interpret [Logseq_sync_pure_reducer.Core.runner_effect] with Eio and + caller-supplied validated dependencies. {!create} binds a runner to an Eio + switch; {!submit} performs I/O and queues exact Core completion events through + [post]. The serial reducer remains the state owner. Asset and protected-value + tickets execute at most once during this runner's lifetime; that process-local + rule is not durable replay evidence. The lifecycle owner calls {!shutdown}. + + Construction depends on the capability types below. Primary excerpts: + {[ + val create : + ?on_asset_diagnostic:(scope:Logseq_sync_pure_reducer.Core.graph_scope + -> operation:string -> request_operation:string + -> Logseq_db_types.Failure_diagnostic.t -> unit) + -> sw:Eio.Switch.t -> dependencies + -> post:(Logseq_sync_pure_reducer.Core.event -> unit) + -> (t, create_error) result + val submit : t -> Logseq_sync_pure_reducer.Core.runner_effect -> unit + val shutdown : t -> unit + ]} *) type t type dependency_error = Invalid_dependency of string type create_error = Invalid_create of string + +(** {1 Minimal usage example} + + The caller supplies [sw], validated [dependencies], a Core-produced [runner_effect], + and [post] that queues later serialized reducer turns: + {[ + match create ~sw dependencies ~post with + | Error error -> Error error + | Ok runner -> + Fun.protect + ~finally:(fun () -> shutdown runner) + (fun () -> + submit runner runner_effect; + run_until_retired runner; + Ok ()) + ]} + [run_until_retired] is the caller's event loop, not a runner API. It keeps the + switch, pump and callback delivery alive through the owner's retirement + protocol. [submit] returning is not the effect's completion acknowledgement. *) + +(** {1 Construction and validation} *) + type runtime val runtime @@ -41,6 +83,8 @@ val transport -> websocket_liveness:websocket_liveness -> (transport, dependency_error) result +(** {2 Storage, secrets and crypto} *) + type local_store val local_store @@ -122,13 +166,20 @@ val create -> post:(Logseq_sync_pure_reducer.Core.event -> unit) -> (t, create_error) result +(** {1 Capability details} *) + (** Asset and protected-value tickets execute at most once for the runner's lifetime. Replaying an already submitted ticket does not execute I/O or post a second completion. *) val submit : t -> Logseq_sync_pure_reducer.Core.runner_effect -> unit +(** {1 Lifecycle and recovery} *) + (** Checked physical cleanup for the original retired logical account. The caller must hold its lifecycle fence and join admitted IO first. Retained native leases preserve their cache and return Error; this issues no authority. *) val retire_account:t -> account:Logseq_sync_pure_reducer.Core.account_scope -> (unit,string)result +(** Stop this runner's admission and cancel owned work. The enclosing switch and + lifecycle owner still own actual I/O/callback joining; this unit return is not + a checked per-account cleanup receipt. *) val shutdown : t -> unit diff --git a/logseq_sync/spec/pure_reducer/asset_transfer.mli b/logseq_sync/spec/pure_reducer/asset_transfer.mli index 60c8626..16dcf25 100644 --- a/logseq_sync/spec/pure_reducer/asset_transfer.mli +++ b/logseq_sync/spec/pure_reducer/asset_transfer.mli @@ -1,6 +1,54 @@ -(** Per-version transfer policy. It never discovers graph assets. *) +(** {1 TLDR} + + Coordinate bounded cache lookup and download demand for explicit asset + versions. The caller owns {!t}; {!step} performs no I/O or persistence and + returns the next state plus ordered {!instruction}s for a runner. It never + discovers graph assets. {!availability} reports per-consumer progress; + successful file handles still require release through emitted instructions. + + The dependent event and instruction variants appear below; these are excerpts + of the actual entry points, not additional declarations: + {[ + val create : config -> scope:Core.graph_scope -> online:bool -> unlocked:bool -> t + val step : t -> event -> t * instruction list + val availability : t -> consumer:string + -> (Logseq_db_types.Graph_types.Uuid.t * availability) list + ]} *) + module Asset = Logseq_db_types.Asset_descriptor +type config + +val config + : active:int + -> foreground_reserved:int + -> pending:int + -> retries:int + -> (config, string) result + +type t + +val create : config -> scope:Core.graph_scope -> online:bool -> unlocked:bool -> t + +(** {1 Minimal usage example} + + The caller supplies validated [config], current [scope], connectivity flags, + an explicit [consumer] and [assets], plus [interpret]: + {[ + let state = ref (create config ~scope ~online ~unlocked) in + let next, instructions = + step !state (Replace { consumer; priority = Foreground; assets }) + in + state := next; + List.iter interpret instructions; + availability !state ~consumer + ]} + [interpret] queues cache/download/timer completions for later serialized turns. + On retirement, feed [Release consumer] (or [Shutdown] for the whole owner), + install its next state and interpret every cleanup instruction the same way. *) + +(** {1 Capability details} *) + type priority = | Foreground | Background @@ -37,6 +85,14 @@ type lookup_source = ; remote_version : Asset.version } +(** {1 Lifecycle and recovery} + + Tickets are created by this reducer for one graph scope, asset and lookup + source/version. The runner returns the exact ticket; {!ticket_current} checks + current ownership before I/O. Replacing demand, version changes and shutdown + can retire work. Stale successful completions may emit [Release_handle] and + must still be interpreted. Tickets are not persisted across restart. *) + type lookup_ticket = private { id : int ; scope : Core.graph_scope @@ -89,18 +145,7 @@ type event = | Unlock_changed of bool | Shutdown -type config - -val config - : active:int - -> foreground_reserved:int - -> pending:int - -> retries:int - -> (config, string) result - -type t - -val create : config -> scope:Core.graph_scope -> online:bool -> unlocked:bool -> t +(** {1 Observation and helpers} *) val availability : t diff --git a/logseq_sync/spec/pure_reducer/core.mli b/logseq_sync/spec/pure_reducer/core.mli index a2e5e4b..19ffe46 100644 --- a/logseq_sync/spec/pure_reducer/core.mli +++ b/logseq_sync/spec/pure_reducer/core.mli @@ -1,4 +1,56 @@ -(** Pure synchronization policy and protocol state. *) +(** {1 TLDR} + + Own pure account, graph and synchronization policy. The host owns {!t}; + {!initial} validates construction and {!step} returns a {!transition} whose + [next] must be installed before interpreting ordered [effects]. [Run] goes + to the Sync runner, [Delegate] to the Worker and [Publish] to observers. + Actual I/O, persistence and callback posting remain with those interpreters. + {!state} exposes startup, unlock, resident graph, network and failure facts. + + The runner GADT and dependent event families appear below. Primary excerpts: + {[ + val initial : config -> (t, create_error) result + val step : t -> event -> transition + val state : t -> state + val scope_for_graph : t -> graph_id:graph_id -> graph_scope option + ]} + Execution, presentation and lifecycle generations are separate. Cancellation + or [Shutdown] is not rollback or a physical join; exact cleanup completions + and [Websocket_retired] acknowledge their actual retained owners. *) + +(** {1 Minimal usage example} + + The caller supplies validated [config], input [event] and [interpret], which + dispatches Run/Delegate/Publish to their existing owners: + {[ + match initial config with + | Error error -> Error error + | Ok first -> + let reducer = ref first in + let transition = step !reducer event in + reducer := transition.next; + List.iter interpret transition.effects; + Ok reducer + ]} + Interpreters queue typed completions for later serialized turns rather than + recursively calling [step]. On retirement feed [Shutdown] and interpret its + effects, while keeping the real I/O and callback owners alive to finish cleanup. *) + +(** {1 Construction and validation} *) + +type limits +type config +type config_error = Invalid_config of string + +val limits + : maximum_response_bytes:int + -> maximum_artifact_bytes:int + -> submission_batch_size:int + -> (limits, config_error) result + +val config : managed_sync_origin:Uri.t -> limits:limits -> (config, config_error) result + +(** {1 Capability details} *) type graph_id = Logseq_db_types.Graph_types.Uuid.t type graph = Logseq_db_types.Managed_graph.t @@ -124,18 +176,6 @@ type state = ; diagnostics : diagnostics } -type limits -type config -type config_error = Invalid_config of string - -val limits - : maximum_response_bytes:int - -> maximum_artifact_bytes:int - -> submission_batch_size:int - -> (limits, config_error) result - -val config : managed_sync_origin:Uri.t -> limits:limits -> (config, config_error) result - type bootstrap_progress = { graph_id : graph_id ; received_bytes : int64 @@ -148,6 +188,14 @@ type invalidation = ; changed_uuids_truncated : bool } +(** {1 Lifecycle and recovery} + + Core allocates execution generations and effect tickets for current owners; + runners hold the original tickets and return matching completions. Scope data + is not authority by itself. Account replacement, graph retirement and lifecycle + changes invalidate ordinary work; retained cleanup owners still require exact + acknowledgements. Process-local tickets are not restart recovery evidence. *) + type account_scope = { managed_sync_origin : Uri.t ; user_id : string @@ -231,6 +279,8 @@ val catalog_cache_selected_graph : catalog_cache -> graph_id option val encode_catalog_cache : catalog_cache -> string val decode_catalog_cache : string -> (catalog_cache, string) result +(** {2 Protected values and assets} *) + type encryption_batch = { scope : graph_scope ; key : graph_key_handle @@ -408,6 +458,8 @@ type protected_ticket val protected_ticket_id : protected_ticket -> string +(** {2 Runner requests and completions} *) + type _ runner_request = | Load_catalog : account_scope -> catalog_cache option runner_request | Save_catalog : @@ -486,6 +538,8 @@ val runner_effect_scope : runner_effect -> effect_scope val equal_runner_effect : runner_effect -> runner_effect -> bool val runner_effect_diagnostic : runner_effect -> string +(** {2 Worker delegation} *) + type mirror_request = { graph : graph ; scope : graph_scope @@ -608,6 +662,8 @@ type timeline_scope = ; graph_generation : graph_generation } +(** {2 Serialized events and transitions} *) + type event = | Host_fence_started of host_fence | Host_fence_released of Logseq_db_types.Graph_types.Uuid.t @@ -686,6 +742,8 @@ type transition = val step : t -> event -> transition +(** {1 Observation and helpers} *) + (** Ordered, currently resident graphs; at most three unique authorized entries. *) val resident_graphs : t -> graph_id list val scope_for_graph : t -> graph_id:graph_id -> graph_scope option diff --git a/logseq_sync/spec/pure_reducer/sync_protocol.mli b/logseq_sync/spec/pure_reducer/sync_protocol.mli index 9c6e8a9..9a7749b 100644 --- a/logseq_sync/spec/pure_reducer/sync_protocol.mli +++ b/logseq_sync/spec/pure_reducer/sync_protocol.mli @@ -1,4 +1,17 @@ -(** Typed application-level WebSocket protocol shared by the sync client and server. *) +(** {1 TLDR} + + Define and encode the bounded application WebSocket protocol in both + directions, without network I/O or persistence. {!Client.message} travels + client to server; {!Server.message} travels server to client. Codecs return + typed {!codec_error}s and reject negative cursors and malformed fields. + + Message variants depend on the payload types below. Primary signature excerpts: + {[ + val encode_client_message : Client.message -> (string, codec_error) result + val decode_client_message : string -> (Client.message, codec_error) result + val encode_server_message : Server.message -> (string, codec_error) result + val decode_server_message : string -> (Server.message, codec_error) result + ]} *) (** A non-negative authoritative transaction cursor. Codec functions reject negative values. *) type cursor = Logseq_db_types.Server_cursor.t @@ -6,6 +19,21 @@ type cursor = Logseq_db_types.Server_cursor.t (** A 16-character hexadecimal entity checksum. *) type checksum = string +(** {1 Minimal usage example} + + A sender encodes a typed message; the receiving endpoint decodes that same + direction. Both failures remain structured rather than exposing raw payloads: + {[ + match encode_client_message Client.Ping with + | Error error -> Error (error_to_string error) + | Ok wire -> + match decode_client_message wire with + | Ok message -> Ok message + | Error error -> Error (error_to_string error) + ]} *) + +(** {1 Capability details} *) + (** A server transaction rejection category. *) type rejection_reason = | Stale @@ -99,6 +127,8 @@ module Server : sig | Error of { message : string } end +(** {1 Observation and helpers} *) + (** The direction in which a rejected wire message travels. *) type direction = | Client