Flyology.DB API reference

Description

Experimental object-native transactional key-value database.

Add_Column_Family

procedure Add_Column_Family
  (Configuration  : Column_Family_Configuration;
   Manifest_ID    : Identifier;
   Transition_ID  : Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Flush_Operation)

Start the same family-registry publication in an established caller-owned checkpoint operation. Configuration and identities are copied before return. Initiating owner/request-shape validation, completion-slot reservation, and lifecycle admission precede moving Payload_Buffer; persisted-state validation then runs in the owner-driven operation. Successful initiation leaves the caller handle vacant until the typed Finish below. No helper task, retry, second deadline, or retained caller input is introduced.

Parameters

Configuration: Exact caller-selected family authority to append
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-operation monotonic timeout budget
Operation: Fresh or consumed client-bound checkpoint operation

Add_Column_Family

procedure Add_Column_Family
  (Item          : in out Database;
   Configuration : Column_Family_Configuration;
   Manifest_ID   : Identifier;
   Transition_ID : Identifier;
   Timeout       : Duration;
   Token         : access Flyology.Cancellation.Token := null;
   Receipt       : out Column_Family_Receipt;
   Result        : out Outcome_Code)

Append one explicit immutable column-family configuration and publish one conditional manifest-bearing HEAD transition. Configuration supplies every key/value, memtable, and L0 authority; the DB selects no defaults. ID must be strictly greater than the current last family ID and Name must be unique. The operation preserves an authenticated post-checkpoint commit suffix without changing the checkpoint replay boundary or identity ledger; confirmed suffix-bearing publication is activated by cacheless recovery. A retained durable checkpoint carrier is required; fresh-root state returns Invalid_State and the DB selects no automatic Flush. This preserves every existing run and reserved identity without selecting new run identities. Manifest_ID and Transition_ID are caller-stable and never reusable after their publication begins. Outcome_Unknown must be resolved with the exact Receipt and never replayed under replacement identities. Success makes the family discoverable through Open_Column_Family.

Parameters

Item: Open current-writer database whose registry is extended
Configuration: Exact caller-selected family authority to append
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Timeout: Whole-operation monotonic timeout budget
Token: Optional cooperative cancellation token
Receipt: Self-contained publication and reconciliation authority
Result: Definite terminal or presently unknown outcome

Begin_Transaction

procedure Begin_Transaction
  (Item           : in out Database;
   Transaction_ID : Transaction_Identifier;
   Isolation      : Isolation_Level;
   Txn            : out Transaction;
   Result         : out Outcome_Code)

Begin one bounded transaction at an explicit isolation level. A Serializable transaction retains distinct external point and half-open range observations up to their independent persisted limits; a legacy manifest without both authorities is rejected as Unsupported_Format. No isolation is inferred.

Parameters

Item: Open database whose current sequence and persisted limits are used
Transaction_ID: Caller-stable never-reused transaction identity
Isolation: Explicit runtime isolation selection
Txn: Vacant transaction output populated only on Success
Result: Success or the exact lifecycle, format, identity, or capacity outcome

Begin_Transaction

procedure Begin_Transaction
  (Item           : in out Database;
   Transaction_ID : Transaction_Identifier;
   Txn            : out Transaction;
   Result         : out Outcome_Code)

Begin one bounded transaction with a caller-stable idempotency identity and capture the current global sequence for later write validation.

Parameters

Item
Transaction_ID
Txn
Result

Byte

subtype Byte is Interfaces.Unsigned_8;

Byte_Array

type Byte_Array is array (Positive range <>) of Byte;

Checkpoint_Requirement_Action

function Checkpoint_Requirement_Action (Item : L0_Checkpoint_Requirement) return L0_Checkpoint_Action

Parameters

Item: Successfully observed checkpoint requirement

Return value

Action captured by the observation

Checkpoint_Requirement_Family

function Checkpoint_Requirement_Family
  (Item : L0_Checkpoint_Requirement; Index : Positive) return Column_Family_ID

Return one exact affected family in stable registry order.

Parameters

Item: Successfully observed checkpoint requirement
Index: One-based affected-family position

Return value

Exact stable column-family ID

Raised exceptions

Constraint_Error: Index is outside the retained family set

Checkpoint_Requirement_Family_Total

function Checkpoint_Requirement_Family_Total (Item : L0_Checkpoint_Requirement) return Natural

Parameters

Item: Successfully observed checkpoint requirement

Return value

Number of exact affected families carried by Item

Checkpoint_Run_Identity

type Checkpoint_Run_Identity is private;

Checkpoint_Run_Identity_Array

type Checkpoint_Run_Identity_Array is array (Positive range <>) of Checkpoint_Run_Identity;

Close

procedure Close (Item : in out Database; Result : out Outcome_Code)

Drain admitted commits, stop and join the coordinator, and close Item.

Parameters

Item
Result

Column_Family

type Column_Family is private;

Column_Family_Configuration

type Column_Family_Configuration is private;

Column_Family_Configuration_Array

type Column_Family_Configuration_Array is array (Positive range <>) of Column_Family_Configuration;

Column_Family_Configuration_ID

function Column_Family_Configuration_ID (Item : Column_Family_Configuration) return Column_Family_ID

Stable persisted numeric family identity.

Parameters

Item: Valid complete family configuration

Return value

Exact persisted family ID

Column_Family_Configuration_Max_Key_Bytes

function Column_Family_Configuration_Max_Key_Bytes
  (Item : Column_Family_Configuration) return Interfaces.Unsigned_64

Exact persisted maximum key extent.

Parameters

Item: Valid complete family configuration

Return value

Exact maximum key bytes

Column_Family_Configuration_Max_Value_Bytes

function Column_Family_Configuration_Max_Value_Bytes
  (Item : Column_Family_Configuration) return Interfaces.Unsigned_64

Exact persisted maximum value extent.

Parameters

Item: Valid complete family configuration

Return value

Exact maximum value bytes

Column_Family_Configuration_Maximum_L0_Runs

function Column_Family_Configuration_Maximum_L0_Runs
  (Item : Column_Family_Configuration) return Interfaces.Unsigned_32

Exact persisted per-family L0-run authority.

Parameters

Item: Valid complete family configuration

Return value

Exact per-family L0-run ceiling

Column_Family_Configuration_Memtable_Max_Bytes

function Column_Family_Configuration_Memtable_Max_Bytes
  (Item : Column_Family_Configuration) return Interfaces.Unsigned_64

Exact persisted logical memtable byte authority.

Parameters

Item: Valid complete family configuration

Return value

Exact memtable byte ceiling

Column_Family_Configuration_Memtable_Max_Entries

function Column_Family_Configuration_Memtable_Max_Entries
  (Item : Column_Family_Configuration) return Interfaces.Unsigned_32

Exact persisted memtable-entry authority.

Parameters

Item: Valid complete family configuration

Return value

Exact memtable entry ceiling

Column_Family_Configuration_Name

function Column_Family_Configuration_Name (Item : Column_Family_Configuration) return Byte_Array

Exact persisted UTF-8 family-name bytes, without normalization.

Parameters

Item: Valid complete family configuration

Return value

Exact persisted family-name bytes

Column_Family_ID

type Column_Family_ID is new Interfaces.Unsigned_32 range 1 .. Interfaces.Unsigned_32'Last;

Column_Family_Receipt

type Column_Family_Receipt is private;

Self-contained exact family-registry publication and reconciliation authority. Its retained immutable bytes are reclaimed automatically.

Column_Family_Receipt_Family_ID

function Column_Family_Receipt_Family_ID (Item : Column_Family_Receipt) return Column_Family_ID

Stable appended family identity carried by Receipt.

Parameters

Item: Family-registry publication receipt

Return value

Exact caller-supplied family ID, or zero before plan admission

Column_Family_Receipt_Manifest_ID

function Column_Family_Receipt_Manifest_ID (Item : Column_Family_Receipt) return Identifier

Stable immutable successor-manifest identity carried by Receipt.

Parameters

Item: Family-registry publication receipt

Return value

Exact caller-supplied manifest ID, or zero before plan admission

Column_Family_Receipt_Outcome

function Column_Family_Receipt_Outcome (Item : Column_Family_Receipt) return Outcome_Code

Outcome most recently assigned to Receipt.

Parameters

Item: Family-registry publication receipt

Return value

Most recent terminal or nonterminal classification

Column_Family_Receipt_Transition_ID

function Column_Family_Receipt_Transition_ID (Item : Column_Family_Receipt) return Identifier

Attempted HEAD transition identity, or zero before conditional HEAD call entry.

Parameters

Item: Family-registry publication receipt

Return value

Exact caller-supplied transition ID or zero

Commit

function Commit
  (Set     : not null access Flyology.Operations.Completion_Set'Class;
   Item    : not null access Database;
   Txn     : in out Transaction;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null) return Commit_Operation'Class

Construct and start one singleton commit in the caller's completion set. Ownership, admission, cancellation, deadline, and certainty match the established operation-last overload.

Parameters

Set: Caller-owned completion set retained through terminal drain
Item: Open database retained through terminal drain
Txn: Active transaction moved only on successful coordinator admission
Timeout: Whole-publication monotonic timeout budget
Token: Optional pre-admission cancellation source retained through drain

Return value

Started singleton commit operation whose dynamic type is Commit_Operation

Raised exceptions

Capacity_Error: Completion set has no reusable operation slot

Commit

procedure Commit
  (Item    : in out Database;
   Txn     : in out Transaction;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Receipt : out Commit_Receipt;
   Result  : out Outcome_Code)

Submit Txn to the bounded long-lived commit coordinator and wait for it. An Outcome_Unknown receipt must be resolved and must never be replayed. Txn is consumed exactly when it is admitted to the coordinator. Rejections detected before admission leave Txn active and rollbackable, including invalid, cancelled, timed-out, conflicting, and capacity outcomes. Every outcome detected after admission consumes Txn. Cancellation no longer applies after admission, and Commit waits for terminal classification. Transaction_ID is also the immutable batch identity for this singleton. A pre-admission outcome returns a receipt with zero transaction/batch IDs; every admitted terminal outcome retains both stable identities. Commit returns Conflict when a written key or retained Serializable point/range predicate intersects a post-Begin write, or when the captured sequence predates retained exact history.

Parameters

Item
Txn
Timeout
Token
Receipt
Result

Commit

procedure Commit (Txn : in out Transaction; Timeout : Duration; Operation : in out Commit_Operation)

Start or restart one singleton commit in an established owner-bound operation. Txn is consumed exactly when the bounded coordinator admits it; every pre-admission outcome leaves Txn active and rollbackable. After admission, cancellation no longer applies and the operation drains to the exact publication classification under the caller's one absolute deadline. No caller transaction borrow remains after return.

Parameters

Txn: Active transaction moved only on successful coordinator admission
Timeout: Whole-publication monotonic timeout budget
Operation: Fresh or consumed database-bound commit operation

Raised exceptions

Capacity_Error: Completion set has no reusable operation slot

Commit_Group

function Commit_Group
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Group_ID     : Identifier;
   Transactions : in out Transaction_Array;
   Timeout      : Duration;
   Token        : access Flyology.Cancellation.Token) return Commit_Group_Operation'Class

Construct and start one atomic transaction group in the caller's completion set. Members derives exactly from Transactions'Length.

Parameters

Set: Caller-owned completion set retained through terminal drain
Item: Open database retained through terminal drain
Group_ID: Caller-stable immutable batch identity
Transactions: Group members moved only on successful atomic admission
Timeout: Whole-publication monotonic timeout budget
Token: Optional pre-admission cancellation source retained through drain

Return value

Started atomic group operation

Raised exceptions

Capacity_Error: Completion set has no reusable operation slot

Commit_Group

procedure Commit_Group
  (Item         : in out Database;
   Group_ID     : Identifier;
   Transactions : in out Transaction_Array;
   Timeout      : Duration;
   Token        : access Flyology.Cancellation.Token := null;
   Receipts     : out Commit_Receipt_Array;
   Result       : out Outcome_Code)

Atomically admit and publish one explicit synchronous transaction group. Transactions and Receipts must have matching lengths of two through Maximum_Group_Transactions members. The whole group shares one absolute deadline, immutable batch, HEAD transition, and terminal classification. All transactions remain active on pre-admission rejection and all are consumed on admission, whatever later terminal outcome is reported. Group members validate writes and retained Serializable predicates independently against external committed history. The explicit group is one atomic co-commit unit, so overlapping member writes remain ordered by their existing deterministic member sequence. Group_ID is the exact immutable batch identity; callers must allocate it from the same never-reused namespace as singleton Transaction_ID values.

Parameters

Item
Group_ID
Transactions
Timeout
Token
Receipts
Result

Commit_Group

procedure Commit_Group
  (Group_ID     : Identifier;
   Transactions : in out Transaction_Array;
   Timeout      : Duration;
   Operation    : in out Commit_Group_Operation)

Start or restart one atomic group in an established owner-bound operation. Transactions must have the structural length selected when Operation was constructed. Pre-admission outcomes retain every member; admission consumes every member and later cancellation drains the exact immutable batch without replay.

Parameters

Group_ID: Caller-stable immutable batch identity
Transactions: Exact operation-sized group member array
Timeout: Whole-publication monotonic timeout budget
Operation: Fresh or consumed database-bound group operation

Raised exceptions

Capacity_Error: Completion set has no reusable operation slot

Commit_Group_Operation

type Commit_Group_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Cancellation : access Flyology.Cancellation.Token;
   Members      : Natural)
is new Flyology.Operations.Operation with private;

Caller-composable atomic group publication. Set, Item, and Cancellation are retained borrows through terminal Finish or abandonment drain. Members is the exact caller-supplied transaction-array length and introduces no capacity: the established two-through- Maximum_Group_Transactions validation is unchanged. No transaction- array borrow survives Start; successful admission moves every member arena atomically before return.

Commit_Operation

type Commit_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable singleton commit publication. Set, Item, and Cancellation are retained borrows and must outlive terminal Finish or abandonment drain. Start performs the existing bounded coordinator admission synchronously: rejection leaves the transaction active, while admission consumes it before Start returns. The long-lived coordinator remains the only worker; this operation adds no helper task, queue, timeout default, retry, or replay path.

Commit_Receipt

type Commit_Receipt is private;

Commit_Receipt_Array

type Commit_Receipt_Array is array (Positive range <>) of Commit_Receipt;

Commit_Resolution_Authority_Length

function Commit_Resolution_Authority_Length (Receipt : Commit_Receipt) return Natural

Exact caller-buffer extent required to export one unresolved Commit reconciliation authority, or zero when Receipt is not a complete Outcome_Unknown authority. The exported bearer record contains the original batch bytes, including application keys and values. It must be stored in caller-provided authenticated, confidential durable storage and bound to the intended higher-level request. Its CRC detects accidental corruption only. This handoff begins after Commit returned Outcome_Unknown; it does not cover interruption inside Commit and does not apply to Create, Add_Column_Family, or Flush receipts.

Parameters

Receipt: Candidate unresolved commit receipt

Return value

Exact export extent, or zero when Receipt is not exportable

Compact

procedure Compact
  (Item          : in out Database;
   Runs          : Checkpoint_Run_Identity_Array;
   Manifest_ID   : Identifier;
   Transition_ID : Identifier;
   Timeout       : Duration;
   Token         : access Flyology.Cancellation.Token;
   Receipt       : out Flush_Receipt;
   Result        : out Outcome_Code)

Publish an exact complete live-state replacement. The caller supplies one fresh output-run identity for every nonempty family; empty families consume no output object or identity, and an all-empty view accepts an empty map. A legacy full family map remains accepted. The operation preserves any later committed suffix and every never-reuse ledger entry, confirms complete immutable outputs before one conditional HEAD transition, and retains superseded objects. It chooses no automatic compaction or deletion policy. Client-backed execution waits on Start_Compaction; memory/files use the equivalent backend-neutral publisher.

Parameters

Item: Open database whose complete live view is compacted
Runs: Exact nonempty-family/output-run identity map
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Timeout: Whole-operation monotonic timeout budget
Token: Cooperative cancellation token, or null for no token
Receipt: Self-contained publication and reconciliation authority
Result: Terminal or presently unknown operation outcome

Compact

procedure Compact
  (Item          : in out Database;
   First_Run_ID  : Identifier;
   Middle_Run_ID : Identifier;
   Last_Run_ID   : Identifier;
   Output_Run_ID : Identifier;
   Manifest_ID   : Identifier;
   Transition_ID : Identifier;
   Timeout       : Duration;
   Token         : access Flyology.Cancellation.Token;
   Receipt       : out Flush_Receipt;
   Result        : out Outcome_Code)

Replace three exact consecutive current runs with one fresh immutable run. Exactly three is the qualified algorithm shape exposed to an explicit caller; it is not a fanout, trigger, or maintenance default. Every selected and publication identity is caller-supplied. The merge retains every version and tombstone, surrounding runs, any later suffix, and every predecessor object. Client-backed execution waits on the matching Start_Compaction overload; memory/files use the equivalent backend-neutral publisher.

Parameters

Item: Open database whose exact consecutive runs are compacted
First_Run_ID: Exact first consecutive current-run identity
Middle_Run_ID: Exact middle consecutive current-run identity
Last_Run_ID: Exact last consecutive current-run identity
Output_Run_ID: Fresh immutable merged-run identity
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Timeout: Whole-operation monotonic timeout budget
Token: Cooperative cancellation token, or null for no token
Receipt: Self-contained publication and reconciliation authority
Result: Terminal or presently unknown operation outcome

Compact

procedure Compact
  (Item          : in out Database;
   Older_Run_ID  : Identifier;
   Newer_Run_ID  : Identifier;
   Output_Run_ID : Identifier;
   Manifest_ID   : Identifier;
   Transition_ID : Identifier;
   Timeout       : Duration;
   Token         : access Flyology.Cancellation.Token;
   Receipt       : out Flush_Receipt;
   Result        : out Outcome_Code)

Replace two exact adjacent current runs with one fresh immutable run. The caller supplies every selected and publication identity. The merge retains every version and tombstone, preserves retained surrounding runs and any later committed suffix, confirms the output and successor before conditional HEAD, and retains predecessor objects. It selects no automatic trigger, level, schedule, retry, pruning, or deletion policy. Client-backed execution waits on the adjacent Start_Compaction overload; memory/files use the equivalent backend-neutral publisher.

Parameters

Item: Open database whose exact adjacent runs are compacted
Older_Run_ID: Exact older adjacent current-run identity
Newer_Run_ID: Exact newer adjacent current-run identity
Output_Run_ID: Fresh immutable merged-run identity
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Timeout: Whole-operation monotonic timeout budget
Token: Cooperative cancellation token, or null for no token
Receipt: Self-contained publication and reconciliation authority
Result: Terminal or presently unknown operation outcome

Configure_Checkpoint_Run

function Configure_Checkpoint_Run
  (Family_ID : Column_Family_ID; Run_ID : Identifier) return Checkpoint_Run_Identity

Bind one configured family to the immutable run identity selected by a checkpoint operation. Run_ID must be nonzero. Flush and complete compaction require one mapping for every family that produces an SST, reject duplicate families or run IDs, and continue accepting a full persisted-family map by ignoring no-work entries. The mapping is borrowed only for the call and is never retained.

Parameters

Family_ID: Stable persisted family identifier
Run_ID: Caller-owned stable immutable run identity

Return value

Valid immutable family/run mapping

Raised exceptions

Constraint_Error: Run_ID is zero

Configure_Column_Family

function Configure_Column_Family
  (ID                   : Column_Family_ID;
   Name                 : Byte_Array;
   Max_Key_Bytes        : Interfaces.Unsigned_64;
   Max_Value_Bytes      : Interfaces.Unsigned_64;
   Memtable_Max_Bytes   : Interfaces.Unsigned_64;
   Memtable_Max_Entries : Interfaces.Unsigned_32;
   Maximum_L0_Runs      : Interfaces.Unsigned_32) return Column_Family_Configuration

Construct one immutable family configuration. Name must contain one to 255 exact UTF-8 bytes and contain no NUL. Key/value and memtable limits plus the per-family L0 run bound must be nonzero. Invalid input raises Constraint_Error before storage effects. These caller-selected values are persisted authority; there are no library defaults.

Parameters

ID
Name
Max_Key_Bytes
Max_Value_Bytes
Memtable_Max_Bytes
Memtable_Max_Entries
Maximum_L0_Runs

Return value

Create

procedure Create
  (Item                  : in out Database;
   Storage               : not null access Storage_Context;
   Database_ID           : Database_Identifier;
   Manifest_ID           : Identifier;
   Initial_Transition_ID : Identifier;
   Limits                : Database_Limits;
   Initial_Families      : Column_Family_Configuration_Array;
   Payload_Buffer        : in out Flyology.Buffers.Unique_Buffer;
   Timeout               : Duration;
   Token                 : access Flyology.Cancellation.Token := null;
   Receipt               : out Create_Receipt;
   Result                : out Outcome_Code)

Create through the owner-driven publication operation while moving one exact caller scratch token. The client-bound path waits the same state machine as the composable form; backend-neutral storage retains the established synchronous implementation. Payload_Buffer is restored before return or propagation of an unexpected local exception.

Parameters

Item: Closed database to create or reconcile idempotently
Storage: Client-bound context, or backend-neutral synchronous context
Database_ID: Exact new database identity
Manifest_ID: Stable immutable root-manifest identity
Initial_Transition_ID: Stable initial HEAD transition identity
Limits: Complete caller-selected persisted database limits
Initial_Families: Complete caller-selected initial family registry
Payload_Buffer: Acquired caller-owned publication/recovery scratch token
Timeout: Whole-create monotonic timeout budget
Token: Optional cooperative cancellation token
Receipt: Exact publication and reconciliation authority
Result: Definite terminal or presently unknown outcome

Create

procedure Create
  (Item                  : in out Database;
   Storage               : not null access Storage_Context;
   Database_ID           : Database_Identifier;
   Manifest_ID           : Identifier;
   Initial_Transition_ID : Identifier;
   Limits                : Database_Limits;
   Initial_Families      : Column_Family_Configuration_Array;
   Timeout               : Duration;
   Token                 : access Flyology.Cancellation.Token := null;
   Receipt               : out Create_Receipt;
   Result                : out Outcome_Code)

Create an empty database and publish its initial HEAD if absent. Item and Storage must remain alive until Close returns.

Parameters

Item
Storage
Database_ID
Manifest_ID
Initial_Transition_ID
Limits
Initial_Families
Timeout
Token
Receipt
Result

Create

procedure Create
  (Database_ID           : Database_Identifier;
   Manifest_ID           : Identifier;
   Initial_Transition_ID : Identifier;
   Limits                : Database_Limits;
   Initial_Families      : Column_Family_Configuration_Array;
   Payload_Buffer        : in out Flyology.Buffers.Unique_Buffer;
   Timeout               : Duration;
   Operation             : in out Create_Operation)

Start or restart one owner-driven initial publication. All caller input is copied into owned manifest/HEAD state before return. Conditional mutation is never replayed; ambiguous admission retains exact receipt authority for Resolve_Create.

Parameters

Database_ID: Exact new database identity copied before return
Manifest_ID: Stable immutable root-manifest identity
Initial_Transition_ID: Stable initial HEAD transition identity
Limits: Complete caller-selected persisted database limits
Initial_Families: Complete caller-selected initial family registry
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-create monotonic timeout budget
Operation: Fresh or consumed client-bound Create operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Create_Operation

type Create_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Storage      : not null access Storage_Context;
   HTTP         : not null access Flyology.HTTP.Client.Client;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable initial database publication. The discriminants are retained borrows and must outlive terminal Finish or abandonment drain. Storage must be bound to the exact HTTP client. Payload_Pool supplies caller-selected publication/reconciliation scratch capacity; the DB introduces no object-size bound, retry, helper task, or timeout default. The worst-case owner stack needs five reusable slots while an existing or ambiguously published HEAD is reconciled: DB Create, DB recovery, Object Storage, HTTP exchange, and transport.

Create_Receipt

type Create_Receipt is private;

Create_Receipt_Manifest_ID

function Create_Receipt_Manifest_ID (Item : Create_Receipt) return Identifier

Stable immutable manifest identity carried by Receipt.

Parameters

Item

Return value

Create_Receipt_Outcome

function Create_Receipt_Outcome (Item : Create_Receipt) return Outcome_Code

Outcome most recently assigned to Receipt.

Parameters

Item

Return value

Create_Receipt_Transition_ID

function Create_Receipt_Transition_ID (Item : Create_Receipt) return Identifier

Attempted HEAD transition identity, or zero before HEAD admission.

Parameters

Item

Return value

Database

type Database is limited private;

Database_Configuration_Snapshot

type Database_Configuration_Snapshot is record
   Registry_Revision : Interfaces.Unsigned_64;
   Family_Count      : Interfaces.Unsigned_32;
   Limits            : Database_Limits;
end record;

One failure-atomic read of the exact installed persisted database configuration. Registry_Revision and Family_Count come from the same authenticated manifest as Limits; this record adds no defaults or mutable policy.

Record fields

Registry_Revision: Exact installed registry revision
Family_Count: Exact installed family total
Limits: Complete installed database-wide limits

Database_Identifier

type Database_Identifier is new Identifier;

Database_Limits

type Database_Limits is record
   Maximum_Column_Families             : Interfaces.Unsigned_32;
   Maximum_Manifest_History            : Interfaces.Unsigned_32;
   Maximum_Batch_History               : Interfaces.Unsigned_32;
   Maximum_Transactions_Per_Batch      : Interfaces.Unsigned_32;
   Maximum_Mutations_Per_Transaction   : Interfaces.Unsigned_32;
   Maximum_Mutations_Per_Batch         : Interfaces.Unsigned_32;
   Maximum_Live_Entries                : Interfaces.Unsigned_32;
   Maximum_Transaction_Payload_Bytes   : Interfaces.Unsigned_64;
   Maximum_Batch_Payload_Bytes         : Interfaces.Unsigned_64;
   Maximum_Live_State_Bytes            : Interfaces.Unsigned_64;
   Maximum_Total_L0_Runs               : Interfaces.Unsigned_32;
   Maximum_Checkpoint_Identities       : Interfaces.Unsigned_32;
   Maximum_Point_Reads_Per_Transaction : Interfaces.Unsigned_32;
   Maximum_Scan_Ranges_Per_Transaction : Interfaces.Unsigned_32;
end record;

Persisted database-wide admission limits. Every field is explicit; the runtime applies no implicit defaults when creating a database.

Record fields

Maximum_Column_Families
Maximum_Manifest_History
Maximum_Batch_History
Maximum_Transactions_Per_Batch
Maximum_Mutations_Per_Transaction
Maximum_Mutations_Per_Batch
Maximum_Live_Entries
Maximum_Transaction_Payload_Bytes
Maximum_Batch_Payload_Bytes
Maximum_Live_State_Bytes
Maximum_Total_L0_Runs
Maximum_Checkpoint_Identities
Maximum_Point_Reads_Per_Transaction: Persisted serializable-observation count authority. Exact point keys and range endpoints remain bounded by their selected family; these database-wide counts add backpressure without a library default.
Maximum_Scan_Ranges_Per_Transaction

Delete

procedure Delete
  (Item     : in out Database;
   Txn      : in out Transaction;
   Family   : Column_Family;
   Item_Key : Byte_Array;
   Result   : out Outcome_Code)

Borrow Item_Key for this call and copy it once into the transaction-owned arena; no caller bytes are retained after return.

Parameters

Item
Txn
Family
Item_Key
Result

Experimental

Experimental : constant Boolean := True;

Project lifecycle classification: the crate is explicitly experimental, so no stable compatibility promise exists. Changing this flag is a release-policy decision, not an implementation detail.

Export_Commit_Resolution_Authority

procedure Export_Commit_Resolution_Authority
  (Receipt   : Commit_Receipt;
   Authority : in out Byte_Array;
   Length    : out Natural;
   Result    : out Outcome_Code)

Export one exact unresolved Commit authority into caller-owned bytes. Authority is unchanged on failure. Length is the exact meaningful prefix on Success and zero otherwise. The operation performs no storage request, changes no receipt, and introduces no retry or replacement identity. Individual Commit_Group member receipts are supported and retain their member-specific transaction identity and sequence.

Parameters

Receipt: Complete unresolved commit authority
Authority: Caller-owned destination retained by the caller
Length: Exact meaningful prefix on Success, zero on failure
Result: Success, Invalid_State, or Capacity_Exceeded

Finish

procedure Finish
  (Operation : in out Commit_Group_Operation;
   Receipts  : out Commit_Receipt_Array;
   Result    : out Outcome_Code)

Consume one terminal owner-driven group and move every retained receipt to the caller's operation-sized array in the original member order.

Parameters

Operation: Terminal composable group operation
Receipts: Exact member-ordered publication authorities
Result: Shared atomic admission/publication outcome

Finish

procedure Finish
  (Operation : in out Commit_Operation; Receipt : out Commit_Receipt; Result : out Outcome_Code)

Consume one terminal owner-driven commit and move its exact retained publication receipt to Receipt. Result preserves the same admitted and pre-admission classifications as the blocking overload.

Parameters

Operation: Terminal composable commit operation
Receipt: Exact publication or reconciliation authority
Result: Exact coordinator admission/publication outcome

Finish

procedure Finish
  (Operation      : in out Create_Operation;
   Receipt        : out Create_Receipt;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume one terminal Create and restore its exact token into any vacant same-pool handle. Receipt remains self-contained for caller-driven reconciliation when Result is Outcome_Unknown.

Parameters

Operation: Terminal caller-owned Create operation
Receipt: Exact publication and reconciliation authority
Result: Definite terminal or presently unknown outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Finish

procedure Finish
  (Operation      : in out Flush_Operation;
   Receipt        : out Column_Family_Receipt;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume a terminal composable family append and restore its exact input token into any vacant same-pool handle. Receipt preserves the same publication and reconciliation authority as the synchronous overload.

Parameters

Operation: Terminal caller-owned checkpoint operation
Receipt: Self-contained publication and reconciliation authority
Result: Definite terminal or presently unknown outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Raised exceptions

Program_Error: Operation contains a Flush result instead

Finish

procedure Finish
  (Operation      : in out Flush_Operation;
   Receipt        : out Flush_Receipt;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume a terminal composable Flush and restore its exact input token. Payload_Buffer may be any vacant handle from the original pool; no pointer to the initiating handle is retained. The restored token keeps its tag and metadata and contains operation scratch bytes. Result and Receipt are the same certainty projection as synchronous Flush. An unexpected retained provider exception is re-raised only after token restoration and operation consumption.

Parameters

Operation: Terminal composable Flush operation
Receipt: Self-contained operation identity and certainty record
Result: Terminal or presently unknown operation outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Raised exceptions

Program_Error: Operation contains a family-append result instead

Finish

procedure Finish
  (Operation      : in out Get_Operation;
   Data           : out Flyology.Bytes.Unbounded_Bytes;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume a terminal owner-driven Get, restore its exact scratch token into any vacant same-pool handle, and return the same Data/Result pair as the synchronous overload. Data is empty on every non-Success outcome. An unexpected retained exception is re-raised only after token and operation ownership are restored.

Parameters

Operation: Terminal fixed-snapshot point read
Data: Owned value bytes, empty on every non-Success outcome
Result: Success, Not_Found, or exact typed failure
Payload_Buffer: Vacant same-pool destination for the exact token

Finish

procedure Finish
  (Operation      : in out Open_Operation;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume one terminal owner-driven open and restore its exact scratch token into any vacant same-pool handle. An unexpected provider exception is re-raised only after ownership restoration and lifecycle cleanup.

Parameters

Operation: Terminal composable open operation
Result: Complete recovery/install or typed failure outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Finish

procedure Finish
  (Operation      : in out Refresh_Operation;
   Receipt        : out Commit_Receipt;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume one terminal owner-driven commit resolution, restore the exact receipt and scratch token, and return the same typed result as the synchronous resolver. Payload_Buffer may be any vacant same-pool handle.

Parameters

Operation: Terminal commit-reconciliation operation
Receipt: Destination receiving the exact moved receipt
Result: Conclusive committed/rejected or still-unknown outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Finish

procedure Finish
  (Operation      : in out Refresh_Operation;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume a terminal owner-driven refresh and restore its exact scratch token. Payload_Buffer may be any vacant handle from the original pool; no pointer to the initiating handle is retained. An unexpected provider exception is re-raised only after ownership restoration and operation consumption.

Parameters

Operation: Terminal composable refresh operation
Result: Monotonic install/no-op or typed failure outcome
Payload_Buffer: Vacant same-pool destination for the exact token

Finish

procedure Finish
  (Operation      : in out Scan_Operation;
   Cursor         : in out Scan_Cursor;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume a terminal authenticated scan initialization. On Success, Cursor atomically receives the new fixed-snapshot position; otherwise it is unchanged. Payload_Buffer may be any vacant handle from the same pool and receives the exact token moved by Start_Scan.

Parameters

Operation: Terminal scan initialization to consume
Cursor: Existing cursor replaced only on Success
Result: Success or exact validation, capacity, storage, or lifecycle outcome
Payload_Buffer: Vacant same-pool handle receiving the exact moved token

Finish

procedure Finish
  (Operation      : in out Scan_Operation;
   Cursor         : in out Scan_Cursor;
   Rows           : in out Scan_Result;
   Done           : out Boolean;
   Result         : out Outcome_Code;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer)

Consume one terminal storage-backed page. Success atomically replaces the exact cursor revision and Rows, and returns the terminal completion flag. Failure preserves both. Payload_Buffer may be any vacant handle from the original pool and receives the exact moved token.

Parameters

Operation: Terminal storage-backed page operation
Cursor: Exact cursor passed to Next_Scan_Page
Rows: Existing result replaced only on Success
Done: True only when this successful page physically exhausts all sources
Result: Success or exact validation, capacity, storage, or lifecycle outcome
Payload_Buffer: Vacant same-pool handle receiving the exact moved token

Flush

procedure Flush
  (Item          : in out Database;
   Runs          : Checkpoint_Run_Identity_Array;
   Manifest_ID   : Identifier;
   Transition_ID : Identifier;
   Timeout       : Duration;
   Token         : access Flyology.Cancellation.Token := null;
   Receipt       : out Flush_Receipt;
   Result        : out Outcome_Code)

Publish an immutable checkpoint at the current committed boundary. The first call writes complete nonempty-family runs; each later call appends one suffix-delta run for every affected family and retains prior current runs. Runs must map every family that has a complete or suffix snapshot to one caller-stable identity. A legacy full family map remains accepted; empty or unchanged entries consume no new run object or identity. Every identity that names an attempted object or HEAD becomes unavailable for reuse once its publication begins. One absolute monotonic deadline covers planning, publication, reconciliation, and local activation. Outcome_Unknown must be resolved and never replayed as a new operation.

Parameters

Item: Open database whose committed prefix is checkpointed
Runs: Exact caller-owned affected-family/run map borrowed for this call
Manifest_ID: Stable immutable checkpoint manifest identity
Transition_ID: Stable attempted HEAD transition identity
Timeout: Whole-operation monotonic timeout budget
Token: Optional cooperative cancellation token
Receipt: Self-contained operation identity and certainty record
Result: Terminal or presently unknown operation outcome

Flush_Operation

type Flush_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Storage      : not null access Storage_Context;
   HTTP         : not null access Flyology.HTTP.Client.Client;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable checkpoint and family-registry publication. The discriminants are retained borrows: Set, Item, Storage, HTTP, Payload_Pool, and Cancellation must outlive terminal Finish or scope-abandonment drain. Storage must be bound to the exact HTTP client. Payload_Pool supplies caller-selected scratch capacity; the DB introduces no body-size default or ceiling. The worst-case owner stack needs five reusable set slots while receipt resolution owns the bounded recovery child: DB Flush, DB recovery, Object Storage, HTTP exchange, and transport. Normal publication and selected-run reads use at most the shorter four-slot prefix.

Flush_Receipt

type Flush_Receipt is private;

Self-contained checkpoint publication and reconciliation state.

Flush_Receipt_Manifest_ID

function Flush_Receipt_Manifest_ID (Item : Flush_Receipt) return Identifier

Stable immutable checkpoint manifest identity carried by Receipt.

Parameters

Item: Flush receipt to inspect

Return value

Exact manifest identity or zero before admission

Flush_Receipt_Outcome

function Flush_Receipt_Outcome (Item : Flush_Receipt) return Outcome_Code

Outcome most recently assigned to Receipt.

Parameters

Item: Flush receipt to inspect

Return value

Most recent certainty-preserving outcome

Flush_Receipt_Replay_Boundary

function Flush_Receipt_Replay_Boundary (Item : Flush_Receipt) return Sequence_Number

Exact committed sequence represented by the checkpoint.

Parameters

Item: Flush receipt to inspect

Return value

Exact replay boundary or zero before admission

Flush_Receipt_Run

function Flush_Receipt_Run (Item : Flush_Receipt; Index : Positive) return Checkpoint_Run_Identity

Return retained family/run mapping Index. Constraint_Error is raised when Index is outside 1 .. Flush_Receipt_Run_Total (Item).

Parameters

Item: Flush receipt to inspect
Index: One-based retained mapping index

Return value

Exact caller-supplied family/run mapping

Raised exceptions

Constraint_Error: Index is outside the retained map

Flush_Receipt_Run_Total

function Flush_Receipt_Run_Total (Item : Flush_Receipt) return Natural

Number of exact family/run mappings retained by Receipt.

Parameters

Item: Flush receipt to inspect

Return value

Retained mapping count or zero before admission

Flush_Receipt_Transition_ID

function Flush_Receipt_Transition_ID (Item : Flush_Receipt) return Identifier

Attempted HEAD transition identity, or zero before storage admission.

Parameters

Item: Flush receipt to inspect

Return value

Exact attempted transition identity or zero

Get

procedure Get
  (Family         : Column_Family;
   Item_Key       : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Get_Operation)

Start or restart the storage-backed form of the same fixed-snapshot point read in an established caller-owned operation. Family and Item_Key are copied before return. Lifecycle and completion-slot admission occur before the exact Payload_Buffer token moves into operation ownership. Successful initiation leaves the caller handle vacant until typed Finish. The operation retains exclusive use of its Txn discriminant while active and records a Serializable point observation only after a conclusive Success or Not_Found result.

Parameters

Family: Valid family handle copied for the fixed read
Item_Key: Exact arbitrary-byte key copied before return
Payload_Buffer: Acquired caller-owned storage scratch token
Timeout: One monotonic budget for the complete read
Operation: Fresh or consumed database/transaction-bound operation

Get

procedure Get
  (Item           : in out Database;
   Txn            : aliased in out Transaction;
   Family         : Column_Family;
   Item_Key       : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Data           : out Flyology.Bytes.Unbounded_Bytes;
   Result         : out Outcome_Code)

Wait on the same owner-driven storage-backed Get state machine. The caller supplies the sole scratch token and whole-operation timeout; the established null cancellation default matches the other DB waits and selects no retry or background execution policy.

Parameters

Item: Open database that owns the fixed snapshot state
Txn: Active transaction borrowed exclusively during this call
Family: Valid family handle
Item_Key: Exact arbitrary-byte key
Payload_Buffer: Acquired caller-owned storage scratch token
Timeout: One monotonic budget for the complete read
Token: Optional cooperative cancellation token
Data: Owned value bytes, empty on every non-Success outcome
Result: Success, Not_Found, or exact typed failure

Get

procedure Get
  (Item     : in out Database;
   Txn      : in out Transaction;
   Family   : Column_Family;
   Item_Key : Byte_Array;
   Data     : out Flyology.Bytes.Unbounded_Bytes;
   Result   : out Outcome_Code)

Read the newest buffered mutation first, then the newest committed value at the transaction's fixed Begin snapshot, into owned bytes. Conflict means the requested snapshot predates retained checkpoint history. Data is empty on every non-Success outcome. A Serializable external read retains its exact family/key predicate on Success or Not_Found; Capacity_Exceeded means a new predicate could not be retained, never that the observation was silently omitted.

Parameters

Item: Open database that owns committed and checkpoint read authority
Txn: Active transaction whose fixed snapshot and observations are used
Family: Valid handle selecting persisted family limits and identity
Item_Key: Exact arbitrary-byte key borrowed only for this call
Data: Owned value bytes, empty on every non-Success outcome
Result: Success, Not_Found, or the exact validation/capacity/lifecycle outcome

Get_Operation

type Get_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Txn          : not null access Transaction;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable fixed-snapshot point read. Item and Txn are retained borrows through terminal publication; the caller must not use Txn while the operation is active. Payload_Pool supplies the sole caller-selected storage scratch bound. The operation checks transaction-local and committed suffix state before reading immutable checkpoint runs, and introduces no helper task, retry, run cap, timeout default, or cache.

Highest_Visible

procedure Highest_Visible (Item : in out Database; Value : out Sequence_Number; Result : out Outcome_Code)

Return the highest sequence confirmed visible while Item is safely open.

Parameters

Item
Value
Result

Identifier

type Identifier is array (Identifier_Index) of Byte;

Identifier_Index

subtype Identifier_Index is Positive range 1 .. Identifier_Length;

Identifier_Length

Identifier_Length   : constant := 16;

Persisted-format authority: every opaque database, transaction, batch, manifest, run, and transition identity is exactly 16 bytes. Widening or narrowing it is incompatible with every existing object format.

Import_Commit_Resolution_Authority

procedure Import_Commit_Resolution_Authority
  (Item      : in out Database;
   Authority : Byte_Array;
   Receipt   : in out Commit_Receipt;
   Result    : out Outcome_Code)

Import one untrusted bearer record into an independently owned unresolved Commit receipt bound to the open Item. Decoding uses Item's authenticated persisted limits and validates the exact database, batch, HEAD transition, member transaction, and member sequence before the receipt is replaced. Authority is borrowed only for this call. Item and Receipt are unchanged on every failure. Success performs no storage request; the resulting receipt is usable only by the existing read-only Resolve operation. CRC validation detects corruption, not a malicious bearer substitution, so callers remain responsible for authenticated, confidential durable storage and higher-level request binding.

Parameters

Item: Open database whose authenticated identity and limits bind the import
Authority: Exact exported bearer bytes borrowed for this call
Receipt: Destination replaced atomically only on Success
Result: Success, Invalid_State, Unsupported_Format, Capacity_Exceeded, or Corrupt

Is_Valid_Column_Family_Configuration

function Is_Valid_Column_Family_Configuration (Item : Column_Family_Configuration) return Boolean

Whether Item carries one complete constructible or persisted family configuration. This predicate selects no fallback values.

Parameters

Item: Family configuration to validate

Return value

True only when every base and LSM field is valid

Isolation_Level

type Isolation_Level is (Snapshot, Serializable);

Transaction isolation selected explicitly at Begin. Snapshot preserves fixed-snapshot write/write validation; Serializable additionally retains exact read predicates for commit-time validation. Enumeration positions are runtime-only and are never persisted or placed on the wire.

Enumeration literals

Snapshot: Fixed snapshot plus write/write validation only
Serializable: Snapshot validation plus retained read predicates

L0_Checkpoint_Action

type L0_Checkpoint_Action is
  (No_L0_Checkpoint_Work, Additive_Flush_Required, Complete_Compaction_Required);

Runtime-only maintenance choice derived from persisted L0 limits and an exact current writer view. Enumeration positions are never persisted or placed on the wire.

Enumeration literals

No_L0_Checkpoint_Work: No committed suffix requires a checkpoint
Additive_Flush_Required: Current runs admit one delta run per changed family
Complete_Compaction_Required: Additive growth is full but a complete run per nonempty family fits

L0_Checkpoint_Requirement

type L0_Checkpoint_Requirement is limited private;

Owned exact-family projection of one checkpoint-action observation. Dynamic storage is derived from the observed persisted registry and is reclaimed automatically; the type retains no Database borrow.

Maximum_Column_Family_Name_Bytes

Maximum_Column_Family_Name_Bytes : constant := 255;

Maximum_Group_Transactions

Maximum_Group_Transactions : constant := 8;

Project admission policy documented by the synchronous topology: one public atomic group has at most eight members. This is a bounded API and coordinator-capacity choice, not a wire-count limit or database default.

Maximum_Initial_Column_Families

Maximum_Initial_Column_Families  : constant := 64;

Current manifest-v1 implementation/reference admission dimensions from the persisted-format contract: 64 family frames and 255 UTF-8 name bytes. They are public creation/name ceilings, not defaults for the persisted Database_Limits fields; changing them requires format, runtime, fixture, and proof compatibility review.

Next_Scan_Page

procedure Next_Scan_Page
  (Item           : in out Database;
   Txn            : aliased in out Transaction;
   Cursor         : in out Scan_Cursor;
   Maximum_Rows   : Interfaces.Unsigned_32;
   Maximum_Bytes  : Interfaces.Unsigned_64;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Rows           : in out Scan_Result;
   Done           : out Boolean;
   Result         : out Outcome_Code)

Blocking wait over the same storage-backed page state machine. All budgets and timeout remain caller-selected. The optional null token is the established convention for no cancellation source, not a retry or deadline policy.

Parameters

Item: Exact open database bound by Cursor
Txn: Exact active transaction and own-mutation version bound by Cursor
Cursor: Active storage-backed cursor advanced only on Success
Maximum_Rows: Caller-selected maximum rows for this page
Maximum_Bytes: Caller-selected maximum key-plus-value bytes
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Caller-selected duration for the complete page
Token: Optional caller-owned cancellation token
Rows: Existing result replaced only on Success
Done: True only when this successful page physically exhausts all sources
Result: Success or exact validation, capacity, storage, or lifecycle outcome

Next_Scan_Page

procedure Next_Scan_Page
  (Item          : in out Database;
   Txn           : in out Transaction;
   Cursor        : in out Scan_Cursor;
   Maximum_Rows  : Interfaces.Unsigned_32;
   Maximum_Bytes : Interfaces.Unsigned_64;
   Rows          : in out Scan_Result;
   Done          : out Boolean;
   Result        : out Outcome_Code)

Materialize the maximal next contiguous page that fits both explicit caller budgets. Maximum_Rows and Maximum_Bytes have no defaults and are per-call backpressure, not persisted or library-selected policy. When a following row does not fit, the maximal nonempty prefix succeeds and remains resumable. When the first remaining indivisible row cannot fit an empty page, Capacity_Exceeded preserves Cursor and Rows exactly. Allocation and validation failure have the same atomic boundary. A valid empty view succeeds with an empty Rows and Done true, including for zero budgets. The final nonempty page also sets Done true; a later call returns Invalid_State. Done is false on every failure. Serializable mode records the complete original range atomically with the first successful page and never consumes another range component.

Parameters

Item: Exact open database bound by Cursor
Txn: Exact active transaction and own-mutation version bound by Cursor
Cursor: Owned fixed-snapshot page position advanced only on Success
Maximum_Rows: Caller-selected maximum rows for this page
Maximum_Bytes: Caller-selected maximum key-plus-value bytes for this page
Rows: Controlled owned page replaced only on Success
Done: True only when this successful page completes the range
Result: Success or the exact validation, capacity, conflict, or lifecycle outcome

Next_Scan_Page

procedure Next_Scan_Page
  (Cursor         : in out Scan_Cursor;
   Maximum_Rows   : Interfaces.Unsigned_32;
   Maximum_Bytes  : Interfaces.Unsigned_64;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Scan_Operation)

Start or restart one storage-backed page. Cursor is borrowed only for validation and exact candidate cloning during this call; the caller must not use or finalize it until typed Finish. One absolute deadline covers every generation-bound next-entry child. Maximum_Rows and Maximum_Bytes are explicit caller backpressure and have no defaults. The operation retains at most one authoritative and one candidate head per immutable run while active. Mutation replay, prefetch, caching, and helper tasks are absent.

Parameters

Cursor: Active storage-backed cursor borrowed through Finish
Maximum_Rows: Caller-selected maximum rows for this page
Maximum_Bytes: Caller-selected maximum key-plus-value bytes
Payload_Buffer: Acquired caller scratch token moved into Operation
Timeout: Caller-selected duration for the complete page
Operation: Fresh or consumed operation receiving retained ownership

Observe_L0_Checkpoint_Requirement

procedure Observe_L0_Checkpoint_Requirement
  (Item : in out Database; Requirement : in out L0_Checkpoint_Requirement; Result : out Outcome_Code)

Atomically replace Requirement with the action and exact affected family IDs from one quiescent writer observation. Additive_Flush_Required carries every suffix-changed family; Complete_Compaction_Required carries every complete-view nonempty family; No_L0_Checkpoint_Work carries none. Failure preserves the prior Requirement. The result reserves no identity and a later commit may invalidate it before publication admission.

Parameters

Item: Open writer database whose current L0 requirement is inspected
Requirement: Owned observation replaced only after complete success
Result: Success or a definite local state/capacity classification

Observe_Range

procedure Observe_Range
  (Item      : in out Database;
   Txn       : in out Transaction;
   Family    : Column_Family;
   Has_Lower : Boolean;
   Lower     : Byte_Array;
   Has_Upper : Boolean;
   Upper     : Byte_Array;
   Result    : out Outcome_Code)

Validate and observe one canonical half-open scan predicate without reading or returning rows. A false endpoint flag means that endpoint is unbounded and its byte argument is ignored. When both endpoints are present, Lower must compare strictly before Upper; an empty or reversed interval returns Invalid_State. Snapshot transactions validate only. Serializable transactions lazily retain normalized same-family components: overlapping or endpoint-touching predicates become their exact union, while cross-family predicates remain distinct. The database's persisted range count bounds components and the selected family's key limit bounds endpoints. Capacity_Exceeded means the exact prior set remains retained. Present endpoint bytes are borrowed only for this call and copied before Success. Scan uses this same endpoint rule.

Parameters

Item: Open database that owns committed conflict history
Txn: Active transaction whose isolation and observations are used
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Result: Success or the exact validation, capacity, or lifecycle outcome

Open

procedure Open
  (Item           : in out Database;
   Storage        : not null access Storage_Context;
   Database_ID    : Database_Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Result         : out Outcome_Code)

Open through the owner-driven recovery operation while moving one exact caller scratch token. This synchronous overload waits the same state machine as the composable form below and restores Payload_Buffer before return or propagation of an unexpected local exception.

Parameters

Item: Closed database to open
Storage: Client-bound object-storage context retained until Close
Database_ID: Exact persisted database identity to authenticate
Payload_Buffer: Acquired caller-owned recovery scratch token
Timeout: Whole-open monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Complete recovery/install or typed failure outcome

Open

procedure Open
  (Item        : in out Database;
   Storage     : not null access Storage_Context;
   Database_ID : Database_Identifier;
   Timeout     : Duration;
   Token       : access Flyology.Cancellation.Token := null;
   Result      : out Outcome_Code)

Open and recover one database solely through HEAD and predecessor batches. Item and Storage must remain alive until Close returns.

Parameters

Item
Storage
Database_ID
Timeout
Token
Result

Open

procedure Open
  (Database_ID    : Database_Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Open_Operation)

Start or restart one cacheless open in an established caller-owned operation. Lifecycle admission and owner validation precede moving the exact Payload_Buffer token. Database_ID is copied before return.

Parameters

Database_ID: Exact persisted database identity to authenticate
Payload_Buffer: Acquired caller-owned recovery scratch token
Timeout: Whole-open monotonic timeout budget
Operation: Fresh or consumed client-bound open operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Open_Column_Family

procedure Open_Column_Family
  (Item : in out Database; Name : Byte_Array; Family : out Column_Family; Result : out Outcome_Code)

Open one stable family handle by its exact persisted UTF-8 name bytes.

Parameters

Item
Name
Family
Result

Open_Column_Family

procedure Open_Column_Family
  (Item : in out Database; ID : Column_Family_ID; Family : out Column_Family; Result : out Outcome_Code)

Open one stable family handle by its persisted numeric ID.

Parameters

Item
ID
Family
Result

Open_Operation

type Open_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Storage      : not null access Storage_Context;
   HTTP         : not null access Flyology.HTTP.Client.Client;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable cacheless open. The discriminants are retained borrows and must outlive terminal Finish or abandonment drain. Storage must be bound to the exact HTTP client. Payload_Pool supplies the caller-selected recovery scratch capacity; the DB introduces no recovery-object bound, helper task, retry, or timeout default. A failed or abandoned operation restores Item to the closed lifecycle state.

Outcome_Code

type Outcome_Code is
  (Success,
   Not_Found,
   Already_Exists,
   Conflict,
   Capacity_Exceeded,
   Invalid_State,
   Timed_Out,
   Cancelled,
   …,
   Stale_Writer);

Enumeration literals

Success
Not_Found
Already_Exists
Conflict
Capacity_Exceeded
Invalid_State
Timed_Out
Cancelled
Outcome_Unknown
Local_Activation_Failed
Unsupported_Format
Corrupt
Storage_Failure
Stale_Writer

Put

procedure Put
  (Item     : in out Database;
   Txn      : in out Transaction;
   Family   : Column_Family;
   Item_Key : Byte_Array;
   Data     : Byte_Array;
   Result   : out Outcome_Code)

Borrow Item_Key/Data for this call and copy them once into the transaction-owned arena; no caller bytes are retained after return.

Parameters

Item
Txn
Family
Item_Key
Data
Result

Read_Configuration

procedure Read_Configuration
  (Item          : in out Database;
   Family        : Column_Family;
   Configuration : in out Column_Family_Configuration;
   Result        : out Outcome_Code)

Replace Configuration with the exact installed settings for Family. Family must belong to Item's current engine incarnation. Failure leaves the caller's prior Configuration unchanged. The returned value combines the authenticated base family record and its persisted LSM extension from one installed engine snapshot.

Parameters

Item: Open database whose installed family authority is inspected
Family: Current family handle to validate
Configuration: Prior value replaced only on Success
Result: Success or the exact validation/lifecycle outcome

Read_Configuration

procedure Read_Configuration
  (Item          : in out Database;
   Configuration : in out Database_Configuration_Snapshot;
   Families      : in out Column_Family_Configuration_Array;
   Result        : out Outcome_Code)

Atomically replace Configuration and the used prefix of Families with one installed registry snapshot. Configuration.Family_Count is the exact used-prefix length; entries are in stable increasing family-ID order. If Families is shorter than that count, Capacity_Exceeded leaves both caller outputs unchanged. Success leaves any excess tail elements unchanged. The call performs no storage I/O, refresh, or dynamic allocation.

Parameters

Item: Open database whose complete installed registry is inspected
Configuration: Prior database snapshot replaced only on Success
Families: Caller-owned capacity whose used prefix is replaced
Result: Success, Capacity_Exceeded, or exact lifecycle outcome

Read_Configuration

procedure Read_Configuration
  (Item          : in out Database;
   Configuration : in out Database_Configuration_Snapshot;
   Result        : out Outcome_Code)

Replace Configuration with the exact installed manifest revision, family count, and persisted database-wide limits. Failure leaves the caller's prior Configuration unchanged. This is a local authoritative snapshot: it performs no storage I/O, refresh, migration, or retry.

Parameters

Item: Open database whose installed manifest is inspected
Configuration: Prior value replaced only on Success
Result: Success or the exact lifecycle/certainty outcome

Read_Scan_Row

procedure Read_Scan_Row
  (Item     : Scan_Result;
   Position : Positive;
   Item_Key : out Flyology.Bytes.Unbounded_Bytes;
   Data     : out Flyology.Bytes.Unbounded_Bytes;
   Result   : out Outcome_Code)

Copy one retained row into caller-owned bytes. Position is one-based in canonical key order. Invalid_State leaves both outputs empty when the position is outside the current result; allocation failure reports Capacity_Exceeded and likewise publishes no partial row.

Parameters

Item: Controlled scan result whose bytes remain owned by Item
Position: One-based row position
Item_Key: Owned exact key bytes, empty on failure
Data: Owned exact value bytes, empty on failure
Result: Success, Invalid_State, or Capacity_Exceeded

Receipt_Batch_ID

function Receipt_Batch_ID (Item : Commit_Receipt) return Identifier

Immutable batch identity retained by the receipt.

Parameters

Item

Return value

Receipt_Outcome

function Receipt_Outcome (Item : Commit_Receipt) return Outcome_Code

Outcome most recently assigned to Receipt.

Parameters

Item

Return value

Receipt_Sequence

function Receipt_Sequence (Item : Commit_Receipt) return Sequence_Number

Sequence assigned to the receipt's transaction, or zero before confirmation.

Parameters

Item

Return value

Receipt_Transaction_ID

function Receipt_Transaction_ID (Item : Commit_Receipt) return Transaction_Identifier

Stable application transaction identity carried by Receipt.

Parameters

Item

Return value

Refresh_Operation

type Refresh_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Storage      : not null access Storage_Context;
   HTTP         : not null access Flyology.HTTP.Client.Client;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable monotonic replica refresh and commit-receipt reconciliation. The discriminants are retained borrows and must outlive terminal Finish or abandonment drain. Storage must be bound to the exact HTTP client. Payload_Pool supplies caller-selected recovery scratch capacity; the DB introduces no body size default or ceiling. The owner stack has the same four-slot geometry as composable checkpoint I/O: DB, Object Storage, HTTP, and transport.

Refresh_Replica

procedure Refresh_Replica
  (Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Refresh_Operation)

Start or restart one owner-driven replica refresh. All validation, operation-slot reservation, and lifecycle admission occur before the exact Payload_Buffer token moves into operation ownership. Every child uses one absolute deadline and the shared recovery request/consume machine; there is no helper task, retry, or retained caller-handle pointer. On an exception during Start, the lifecycle and slot roll back and Payload_Buffer is restored byte/tag/metadata/length exact.

Parameters

Payload_Buffer: Acquired caller-owned recovery scratch token
Timeout: Whole-refresh monotonic timeout budget
Operation: Fresh or consumed client-bound refresh operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Refresh_Replica

procedure Refresh_Replica
  (Item    : in out Database;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Result  : out Outcome_Code)

Perform one caller-triggered monotonic refresh of an open handle used as a read-only replica. The caller must finish every transaction and other operation on Item before calling. Refresh validates a complete authoritative recovery graph and atomically installs it only when its transition-number/writer-epoch pair is newer than the installed pair; observing the same or an older valid pair succeeds without changing the local view. Allocation or recovery failure preserves the prior view. This call neither polls nor retries and never promotes a fenced handle; Stale_Writer remains terminal for that handle. Timeout is the caller's one monotonic budget, and Token supplies optional cooperative cancellation. The operation selects no replica lease, cadence, registration, retention, or promotion policy.

Parameters

Item: Open caller-designated read-only replica handle to refresh
Timeout: Whole-refresh monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Monotonic install/no-op or typed failure outcome

Required_L0_Checkpoint_Action

procedure Required_L0_Checkpoint_Action
  (Item : in out Database; Action : out L0_Checkpoint_Action; Result : out Outcome_Code)

Inspect the exact quiescent writer view and report the next L0 action implied solely by persisted per-family and database-wide run ceilings. The call serializes with commit/checkpoint lifecycle work but performs no storage I/O, reserves no publication identity, and starts no background task. A later commit can change the answer; Flush and Compact therefore revalidate every bound and publication precondition. On Capacity_Exceeded neither additive Flush nor complete compaction can fit; Action is only meaningful when Result is Success.

Parameters

Item: Open writer database whose current L0 requirement is inspected
Action: Exact current action selected from persisted run authorities
Result: Success or a definite local state/capacity classification

Resolve

procedure Resolve
  (Receipt        : in out Commit_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Refresh_Operation)

Start exact commit-receipt reconciliation in an established recovery operation. Receipt and Payload_Buffer move into Operation until the receipt-returning typed Finish. The operation drains admitted local work, validates one complete authoritative recovery graph, and matches the retained exact batch bytes or a conclusive successor transition. It never republishes the batch or HEAD and introduces no retry, helper task, replacement identity, or second deadline.

Parameters

Receipt: Original unresolved commit receipt moved until Finish
Payload_Buffer: Acquired caller-owned recovery scratch token
Timeout: Whole-resolution monotonic timeout budget
Operation: Fresh or consumed client-bound recovery operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match receipt storage

Resolve

procedure Resolve
  (Item    : in out Database;
   Receipt : in out Commit_Receipt;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Result  : out Outcome_Code)

Reconcile the exact batch and HEAD transition retained by Receipt.

Parameters

Item
Receipt
Timeout
Token
Result

Resolve

procedure Resolve
  (Item           : in out Database;
   Storage        : not null access Storage_Context;
   Receipt        : in out Commit_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Result         : out Outcome_Code)

Blocking wait over the same client-bound commit resolver. The exact receipt and caller scratch token are restored before return. A storage-neutral binding retains the established direct resolver.

Parameters

Item: Open database retained by the original commit
Storage: Exact client-bound storage owned by Item
Receipt: Original unresolved receipt, updated in place
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Conclusive committed/rejected or still-unknown outcome

Resolve_Add_Column_Family

procedure Resolve_Add_Column_Family
  (Receipt        : in out Column_Family_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Flush_Operation)

Start exact receipt-driven family-publication reconciliation in an established provider-bound checkpoint operation. Receipt and Payload_Buffer move into Operation until typed family Finish. Immutable uncertainty confirms the retained exact manifest before the one permitted same-identity HEAD admission; HEAD uncertainty performs only bounded authenticated recovery. No new identity, helper task, replay, retry policy, or second deadline is introduced.

Parameters

Receipt: Original nonterminal family receipt moved until Finish
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-resolution monotonic timeout budget
Operation: Fresh or consumed client-bound checkpoint operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Receipt or buffer ownership

Resolve_Add_Column_Family

procedure Resolve_Add_Column_Family
  (Item    : in out Database;
   Receipt : in out Column_Family_Receipt;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Result  : out Outcome_Code)

Continue exact immutable-manifest confirmation or reconcile the attempted HEAD retained by Receipt. No identity, configuration, or bytes change.

Parameters

Item: Same open database retained by the original append attempt
Receipt: Original nonterminal receipt, updated in place
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Terminal or still-unknown resolution outcome

Resolve_Add_Column_Family

procedure Resolve_Add_Column_Family
  (Item           : in out Database;
   Storage        : not null access Storage_Context;
   Receipt        : in out Column_Family_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Result         : out Outcome_Code)

Blocking wait over the same provider-bound family resolver. The exact receipt and caller scratch token are restored before return. Backend- neutral storage retains the established direct resolver until those providers expose caller-driven children.

Parameters

Item: Same open database retained by the original append
Storage: Exact storage binding owned by Item
Receipt: Original nonterminal family receipt, updated in place
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Terminal or still-unknown resolution outcome

Resolve_Create

procedure Resolve_Create
  (Receipt        : in out Create_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Create_Operation)

Start or restart receipt-driven Create resolution on the same provider- owned state machine as Create. The exact receipt authority and scratch token move into Operation until typed Finish. A confirmed manifest may admit its exact HEAD mutation once; an unknown HEAD is reconciled only by reads and is never replayed.

Parameters

Receipt: Exact resumable Create publication authority moved until Finish
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-resolution monotonic timeout budget
Operation: Fresh or consumed client-bound Create operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Resolve_Create

procedure Resolve_Create
  (Item           : in out Database;
   Storage        : not null access Storage_Context;
   Receipt        : in out Create_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Result         : out Outcome_Code)

Resume or reconcile Create through the owner-driven operation while moving one exact caller scratch token. Client-bound execution waits the same state machine as the composable overload; backend-neutral storage retains the established direct synchronous implementation.

Parameters

Item: Closed database to activate after conclusive resolution
Storage: Exact storage binding retained by an activated database
Receipt: Exact resumable Create publication authority
Payload_Buffer: Acquired caller-owned resolution scratch token
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Definite terminal or presently unknown outcome

Resolve_Create

procedure Resolve_Create
  (Item    : in out Database;
   Storage : not null access Storage_Context;
   Receipt : in out Create_Receipt;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Result  : out Outcome_Code)

Resume a confirmed-manifest creation before HEAD admission, or reconcile a possibly admitted HEAD publication without replaying it.

Parameters

Item
Storage
Receipt
Timeout
Token
Result

Resolve_Flush

procedure Resolve_Flush
  (Item    : in out Database;
   Receipt : in out Flush_Receipt;
   Timeout : Duration;
   Token   : access Flyology.Cancellation.Token := null;
   Result  : out Outcome_Code)

Continue exact immutable-object reconciliation or reconcile the attempted HEAD retained by Receipt. Resolve_Flush never changes an identity and never republishes application work under a new identity.

Parameters

Item: Same open database retained by the original Flush
Receipt: Original nonterminal Flush receipt, updated in place
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Terminal or still-unknown resolution outcome

Resolve_Flush

procedure Resolve_Flush
  (Item           : in out Database;
   Storage        : not null access Storage_Context;
   Receipt        : in out Flush_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Result         : out Outcome_Code)

Blocking wait over the same provider-bound Resolve_Flush state machine. The exact receipt and caller scratch token are restored before return. Backend-neutral storage retains the established direct resolver until those providers expose caller-driven children.

Parameters

Item: Same open database retained by the original Flush
Storage: Exact storage binding owned by Item
Receipt: Original nonterminal Flush receipt, updated in place
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Whole-resolution monotonic timeout budget
Token: Optional cooperative cancellation token
Result: Terminal or still-unknown resolution outcome

Resolve_Flush

procedure Resolve_Flush
  (Receipt        : in out Flush_Receipt;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Flush_Operation)

Start exact receipt-driven Flush reconciliation in an established provider-bound operation. Receipt and Payload_Buffer move into Operation and remain owned there until typed Finish. Objects_Unknown reconstructs and authenticates the original immutable bytes before continuing their same-identity publication; HEAD uncertainty performs read-only recovery and local activation. No identity, application work, helper task, retry policy, or second deadline is introduced.

Parameters

Receipt: Original nonterminal Flush receipt moved until Finish
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-resolution monotonic timeout budget
Operation: Fresh or consumed client-bound Flush operation

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Receipt or buffer ownership

Rollback

procedure Rollback (Txn : in out Transaction; Result : out Outcome_Code)

Consume an active transaction without publishing it.

Parameters

Txn
Result

Scan

procedure Scan
  (Item           : in out Database;
   Txn            : aliased in out Transaction;
   Family         : Column_Family;
   Has_Lower      : Boolean;
   Lower          : Byte_Array;
   Has_Upper      : Boolean;
   Upper          : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Rows           : in out Scan_Result;
   Result         : out Outcome_Code)

Materialize a complete authenticated fixed-snapshot interval by waiting on the storage-backed Scan_Operation initialization, then requesting one complete page from that cursor's established physical merge engine. One absolute timeout covers both phases. Persisted live-row and live-byte limits are the complete-page budgets; no page default, second storage path, helper task, retry, or additional capacity is introduced. Rows is replaced only on Success, and Payload_Buffer is always restored.

Parameters

Item: Open client-bound database owning the fixed snapshot
Txn: Active transaction retained for the duration of the call
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Caller-selected duration for the complete authenticated scan
Token: Optional caller-owned cancellation token
Rows: Controlled owned result replaced only on Success
Result: Success or the exact validation, capacity, storage, or lifecycle outcome

Scan

procedure Scan
  (Item      : in out Database;
   Txn       : in out Transaction;
   Family    : Column_Family;
   Has_Lower : Boolean;
   Lower     : Byte_Array;
   Has_Upper : Boolean;
   Upper     : Byte_Array;
   Rows      : in out Scan_Result;
   Result    : out Outcome_Code)

Materialize every live row in one canonical half-open family interval at Txn's fixed snapshot, ordered by unsigned-byte lexicographic key. Endpoint flags and validation match Observe_Range. Exact row count and key-plus-value bytes are bounded by the database's persisted live-state limits; individual extents remain bounded by the selected family. There is no page size, byte default, timeout, storage I/O, or helper task. The implementation captures and completes the same owned physical cursor used by Next_Scan_Page; no cursor state escapes this call. Rows is replaced atomically only on Success and remains unchanged on every failure. A Serializable success merges the exact predicate into its normalized retained components only after complete materialization; failure publishes neither rows nor a predicate. Endpoint bytes are borrowed only for this call.

Parameters

Item: Open database that owns fixed-snapshot state
Txn: Active transaction whose snapshot and own mutations are read
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Rows: Controlled owned result replaced only on Success
Result: Success or the exact validation, capacity, conflict, or lifecycle outcome

Scan_Cursor

type Scan_Cursor is limited private;

Limited owned fixed-snapshot page position. It copies range endpoints and retains identity/version facts only; no Database, Transaction, Column_Family, or caller-array access value survives Start_Scan.

Scan_Operation

type Scan_Operation
  (Set          : not null access Flyology.Operations.Completion_Set'Class;
   Item         : not null access Database;
   Txn          : not null access Transaction;
   Payload_Pool : not null access Flyology.Buffers.Pool;
   Cancellation : access Flyology.Cancellation.Token)
is new Flyology.Operations.Operation with private;

Caller-composable authenticated fixed-snapshot scan initialization or storage-backed page advancement. Item and Txn are retained borrows through terminal publication; the caller must not use Txn while the operation is active. Payload_Pool supplies the sole caller-selected object-read scratch bound. The established Start_Scan form reads each run's canonical snapshot-visible entries through generation-bound next-entry reads and creates the same owned materialized cursor used by storage-free Next_Scan_Page. Start_Storage_Backed_Scan instead retains exact run descriptors plus in-memory sources; the composable Next_Scan_Page overload fetches at most one authenticated current head per immutable run while building a page. Neither form introduces a helper task, mutation retry, run cap, page default, prefetch, or cache.

Scan_Result

type Scan_Result is limited private;

Limited owned materialization replaced atomically by Scan. Its dynamic storage is bounded only by persisted database/family authorities and is reclaimed automatically; the type introduces no copy or default limit.

Scan_Row_Count

function Scan_Row_Count (Item : Scan_Result) return Natural

Number of live rows retained by Item, including zero for a fresh or successfully empty result.

Parameters

Item: Controlled scan result

Return value

Exact retained row count

Sequence_Number

type Sequence_Number is new Interfaces.Unsigned_64;

Start_Compaction

procedure Start_Compaction
  (Operation      : in out Flush_Operation;
   Runs           : Checkpoint_Run_Identity_Array;
   Manifest_ID    : Identifier;
   Transition_ID  : Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration)

Start an exact complete-view compaction in an established operation. Runs maps every nonempty family to a caller-selected fresh output identity; an all-empty replacement accepts an empty map. A legacy full family map remains accepted and its empty-family entries are ignored. Compaction copies Runs and retains no borrow of that map after return. It removes no stored predecessor and selects no trigger, level, fanout, schedule, retry, or garbage-collection policy. Its normal operation-owner borrows and the moved Payload_Buffer remain retained until Finish or finalization drain. Ownership, deadline, certainty, and exact same-identity reconciliation are identical to Start_Flush.

Parameters

Operation: Fresh or consumed client-bound checkpoint operation
Runs: Exact nonempty-family/output-run identity map copied before return
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-operation monotonic timeout budget

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Start_Compaction

procedure Start_Compaction
  (Operation      : in out Flush_Operation;
   Older_Run_ID   : Identifier;
   Newer_Run_ID   : Identifier;
   Output_Run_ID  : Identifier;
   Manifest_ID    : Identifier;
   Transition_ID  : Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration)

Start an exact caller-selected adjacent-run compaction. Older_Run_ID and Newer_Run_ID must name adjacent current descriptors in one family; Output_Run_ID, Manifest_ID, and Transition_ID are fresh caller-stable identities. Every version and tombstone is retained, including through a later committed suffix. The operation selects no pair, trigger, level, schedule, retry, retention horizon, or deletion policy. Runs are authenticated and copied into operation-owned state; no caller ID borrow survives return. Normal operation-owner borrows and the moved Payload_Buffer remain until Finish or finalization drain.

Parameters

Operation: Fresh or consumed client-bound checkpoint operation
Older_Run_ID: Exact older adjacent current-run identity
Newer_Run_ID: Exact newer adjacent current-run identity
Output_Run_ID: Fresh immutable merged-run identity
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-operation monotonic timeout budget

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Start_Compaction

procedure Start_Compaction
  (Operation      : in out Flush_Operation;
   First_Run_ID   : Identifier;
   Middle_Run_ID  : Identifier;
   Last_Run_ID    : Identifier;
   Output_Run_ID  : Identifier;
   Manifest_ID    : Identifier;
   Transition_ID  : Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration)

Start an exact caller-selected three-run compaction. First_Run_ID, Middle_Run_ID, and Last_Run_ID must name three consecutive current descriptors in one family. Exactly three is the already-qualified algorithm shape, not an automatic fanout or policy default. The merge retains every version and tombstone, preserves surrounding runs and any later committed suffix, and selects no trigger, level, schedule, retry, retention horizon, pruning, or deletion policy. Selected identities are copied into operation-owned state; no caller ID borrow survives return.

Parameters

Operation: Fresh or consumed client-bound checkpoint operation
First_Run_ID: Exact first consecutive current-run identity
Middle_Run_ID: Exact middle consecutive current-run identity
Last_Run_ID: Exact last consecutive current-run identity
Output_Run_ID: Fresh immutable merged-run identity
Manifest_ID: Stable immutable successor-manifest identity
Transition_ID: Stable attempted HEAD transition identity
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-operation monotonic timeout budget

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Start_Flush

procedure Start_Flush
  (Operation      : in out Flush_Operation;
   Runs           : Checkpoint_Run_Identity_Array;
   Manifest_ID    : Identifier;
   Transition_ID  : Identifier;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration)

Start checkpoint publication in an established operation. All initiating owner and request-shape validation, pool compatibility, completion-slot reservation, and lifecycle admission precede ownership transfer. Successful Start moves Payload_Buffer's exact token into Operation and leaves the caller handle vacant until typed Finish. Insufficient caller-selected block capacity is a definite prepublication Capacity_Exceeded result. No helper task, hidden retry, or second deadline is introduced.

Parameters

Operation: Fresh or consumed client-bound Flush operation
Runs: Exact affected-family/run identity map copied before return
Manifest_ID: Stable immutable checkpoint manifest identity
Transition_ID: Stable attempted HEAD transition identity
Payload_Buffer: Acquired caller-owned scratch token moved until Finish
Timeout: Whole-operation monotonic timeout budget

Raised exceptions

Capacity_Error: Completion set has no reusable parent slot
Program_Error: Operation owners do not match Storage binding

Start_Scan

procedure Start_Scan
  (Family         : Column_Family;
   Has_Lower      : Boolean;
   Lower          : Byte_Array;
   Has_Upper      : Boolean;
   Upper          : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Scan_Operation)

Start or restart authenticated object-storage initialization of one fixed-snapshot cursor. The exact manifest run slice is traversed one authenticated next entry at a time under one absolute monotonic deadline and caller-bounded scratch, then merged with the captured committed suffix and transaction-local mutations. Payload_Buffer moves into Operation only after validation and operation admission. Typed Finish is the sole restoration and cursor-publication authority. Any failure preserves the caller's prior cursor exactly.

Parameters

Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Payload_Buffer: Acquired caller scratch token moved into Operation
Timeout: Caller-selected duration for the complete initialization
Operation: Fresh or consumed operation receiving retained ownership

Start_Scan

procedure Start_Scan
  (Item           : in out Database;
   Txn            : aliased in out Transaction;
   Family         : Column_Family;
   Has_Lower      : Boolean;
   Lower          : Byte_Array;
   Has_Upper      : Boolean;
   Upper          : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Cursor         : in out Scan_Cursor;
   Result         : out Outcome_Code)

Blocking wait over the same authenticated scan-initialization state machine. The optional null cancellation token follows the established Flyology operation convention and selects no timeout or retry policy.

Parameters

Item: Open client-bound database owning the fixed snapshot
Txn: Active transaction retained for the duration of the call
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Caller-selected duration for the complete initialization
Token: Optional caller-owned cancellation token
Cursor: Existing cursor replaced only on Success
Result: Success or exact validation, capacity, storage, or lifecycle outcome

Start_Scan

procedure Start_Scan
  (Item      : in out Database;
   Txn       : in out Transaction;
   Family    : Column_Family;
   Has_Lower : Boolean;
   Lower     : Byte_Array;
   Has_Upper : Boolean;
   Upper     : Byte_Array;
   Cursor    : in out Scan_Cursor;
   Result    : out Outcome_Code)

Start or restart one fixed-snapshot paged scan. Endpoint rules and family validation are identical to Scan. Before Success the cursor owns exact ordered descriptors, retained immutable image leases, copied own mutations, and present endpoints; failure preserves the prior Cursor exactly. The cursor binds Txn's fixed committed snapshot and current own-mutation version. A later successful Put/Delete invalidates subsequent page calls instead of mixing transaction views. This call materializes no result rows and records no Serializable predicate.

Parameters

Item: Open database that owns fixed-snapshot state
Txn: Active transaction whose snapshot and own writes are fixed
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Cursor: Owned page position replaced only on Success
Result: Success or the exact validation, capacity, or lifecycle outcome

Start_Storage_Backed_Scan

procedure Start_Storage_Backed_Scan
  (Family         : Column_Family;
   Has_Lower      : Boolean;
   Lower          : Byte_Array;
   Has_Upper      : Boolean;
   Upper          : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Operation      : in out Scan_Operation)

Start or restart one authenticated storage-backed cursor initialization. Unlike Start_Scan, this form does not traverse every selected immutable run before publication. It retains exact run descriptors, committed in-memory sources, transaction-local bytes, endpoints, and identity/version authority. Later object reads occur only through the composable Next_Scan_Page overload. No result row or Serializable predicate is published here.

Parameters

Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Payload_Buffer: Acquired caller scratch token moved into Operation
Timeout: Caller-selected duration for initialization
Operation: Fresh or consumed operation receiving retained ownership

Start_Storage_Backed_Scan

procedure Start_Storage_Backed_Scan
  (Item           : in out Database;
   Txn            : aliased in out Transaction;
   Family         : Column_Family;
   Has_Lower      : Boolean;
   Lower          : Byte_Array;
   Has_Upper      : Boolean;
   Upper          : Byte_Array;
   Payload_Buffer : in out Flyology.Buffers.Unique_Buffer;
   Timeout        : Duration;
   Token          : access Flyology.Cancellation.Token := null;
   Cursor         : in out Scan_Cursor;
   Result         : out Outcome_Code)

Blocking wait over the same storage-backed initialization state machine. The caller selects the sole scratch token and timeout; the optional null cancellation token is the established Flyology convention and introduces no retry or hidden deadline.

Parameters

Item: Open client-bound database owning the fixed snapshot
Txn: Active transaction retained for the duration of the call
Family: Valid handle selecting persisted family limits and identity
Has_Lower: True when Lower is the inclusive endpoint
Lower: Inclusive endpoint bytes, ignored when Has_Lower is false
Has_Upper: True when Upper is the exclusive endpoint
Upper: Exclusive endpoint bytes, ignored when Has_Upper is false
Payload_Buffer: Acquired caller scratch token restored before return
Timeout: Caller-selected duration for initialization
Token: Optional caller-owned cancellation token
Cursor: Existing cursor replaced only on Success
Result: Success or exact validation, capacity, storage, or lifecycle outcome

Storage_Context

type Storage_Context is limited private;

Transaction

type Transaction is limited private;

Transaction_Array

type Transaction_Array is array (Positive range <>) of Transaction;

Transaction_Identifier

type Transaction_Identifier is new Identifier;

Zero_Database_ID

Zero_Database_ID    : constant Database_Identifier := [others => 0];

Public typed forms of the same frozen absence sentinel; they add no separate namespace policy or wire representation.

Zero_Identifier

Zero_Identifier     : constant Identifier := [others => 0];

Persisted semantic sentinel: the all-zero identity means absent and is rejected wherever a definite identity is required. Reclassifying it as usable would invalidate structural and nonreuse rules.

Zero_Transaction_ID

Zero_Transaction_ID : constant Transaction_Identifier := [others => 0];