ic-sqlite-vfs 2.0.0

SQLite VFS backed directly by Internet Computer stable memory
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

//! Verus model for v8 no-op compact invariants.
//!
//! The public compact API remains available, but the in-place layout does not
//! rewrite page data or metadata beyond rejecting unsupported layout versions.
//!
//! Capacity proof mapping:
//! - T6: compact is no-op, not reclaim, and preserves resource high water.

use vstd::prelude::*;

verus! {

struct Image {
    db_base_offset: nat,
    db_size: nat,
    page_table_offset: nat,
    page_table_bytes: nat,
    page_count: nat,
    allocated_bytes: nat,
    high_water_mark: nat,
    orphan_bytes_estimate: nat,
    compact_recommended: bool,
    checksum: nat,
    last_tx_id: nat,
}

struct StorageStats {
    allocated_bytes: nat,
    high_water_mark: nat,
    orphan_bytes_estimate: nat,
    compact_recommended: bool,
}

spec fn compact(image: Image) -> Image {
    image
}

spec fn storage_stats_for_v8(image: Image) -> StorageStats {
    StorageStats {
        allocated_bytes: image.allocated_bytes,
        high_water_mark: image.high_water_mark,
        orphan_bytes_estimate: image.orphan_bytes_estimate,
        compact_recommended: false,
    }
}

proof fn compact_preserves_db_base_offset(image: Image)
    ensures
        compact(image).db_base_offset == image.db_base_offset,
{
}

proof fn compact_preserves_logical_size(image: Image)
    ensures
        compact(image).db_size == image.db_size,
        compact(image).page_count == image.page_count,
{
}

proof fn compact_preserves_page_table_absence(image: Image)
    ensures
        compact(image).page_table_offset == image.page_table_offset,
        compact(image).page_table_bytes == image.page_table_bytes,
{
}

proof fn compact_preserves_resource_high_water(image: Image)
    ensures
        compact(image).allocated_bytes == image.allocated_bytes,
        compact(image).high_water_mark == image.high_water_mark,
        compact(image).orphan_bytes_estimate == image.orphan_bytes_estimate,
        compact(image).compact_recommended == image.compact_recommended,
{
}

proof fn compact_never_recommends_reclaim(image: Image)
    requires
        image.compact_recommended == false,
    ensures
        compact(image).compact_recommended == false,
{
}

proof fn v8_storage_stats_never_recommend_compact(image: Image)
    ensures
        storage_stats_for_v8(image).compact_recommended == false,
        storage_stats_for_v8(compact(image)).compact_recommended == false,
        storage_stats_for_v8(compact(image)).allocated_bytes
            == storage_stats_for_v8(image).allocated_bytes,
        storage_stats_for_v8(compact(image)).orphan_bytes_estimate
            == storage_stats_for_v8(image).orphan_bytes_estimate,
{
}

proof fn compact_preserves_checksum_metadata(image: Image)
    ensures
        compact(image).checksum == image.checksum,
        compact(image).last_tx_id == image.last_tx_id,
{
}

}