oxgraph-postgres 0.3.2

Postgres-backed OxGraph engine: catalog, build, artifact I/O, query, sync.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

//! Kani proofs for bounded Postgres engine contracts.
//!
//! Overlay/sync replay proofs are skipped — unbounded `Vec` growth in harnesses.

#![cfg(kani)]

use zerocopy::{FromBytes, IntoBytes};

use crate::{artifact::PostgresMetadata, role::GraphRole, sync::SyncAction};

/// `GraphRole` equality is reflexive on the two variants.
#[kani::proof]
fn graph_role_reflexive() {
    let role: GraphRole = if kani::any() {
        GraphRole::Reader
    } else {
        GraphRole::Admin
    };
    assert_eq!(role, role);
}

/// `SyncAction` equality is reflexive for bounded symbolic variants.
#[kani::proof]
fn sync_action_reflexive() {
    let action = if kani::any() {
        SyncAction::InsertEdge {
            source: kani::any(),
            target: kani::any(),
        }
    } else if kani::any() {
        SyncAction::DeleteEdge {
            edge_id: kani::any(),
        }
    } else if kani::any() {
        SyncAction::DeleteNode {
            node_id: kani::any(),
        }
    } else {
        SyncAction::TruncateOverlays
    };
    assert_eq!(action, action);
}

/// `PostgresMetadata::new` round-trips through zerocopy layout bytes.
#[kani::proof]
fn postgres_metadata_roundtrip() {
    let node_count: u32 = kani::any();
    let edge_count: u32 = kani::any();
    let built_at: u64 = kani::any();
    let read_only: bool = kani::any();
    let meta = PostgresMetadata::new(node_count, edge_count, built_at, read_only);
    let bytes = meta.as_bytes();
    let parsed = PostgresMetadata::read_from_bytes(bytes);
    assert_eq!(parsed.ok(), Some(meta));
}