ic-sqlite-vfs 0.2.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
103
104
105
106

//! Verus model for SQLite stable-memory layout arithmetic.
//!
//! This proof file intentionally stays separate from production Rust. It checks
//! arithmetic invariants for the layout model; Rust tests compare boundary
//! behavior against production helpers.

use vstd::prelude::*;

verus! {

spec fn sqlite_page_size() -> nat {
    16_384
}

spec fn segment_page_count() -> nat {
    256
}

spec fn page_table_entry_len() -> nat {
    8
}

spec fn u64_max() -> nat {
    18_446_744_073_709_551_615
}

spec fn page_count_for_size(size: nat) -> nat {
    if size == 0 {
        0
    } else {
        (((size - 1) / (sqlite_page_size() as int)) + 1) as nat
    }
}

spec fn segment_count_for_pages(page_count: nat) -> nat {
    if page_count == 0 {
        0
    } else {
        (((page_count - 1) / (segment_page_count() as int)) + 1) as nat
    }
}

spec fn segment_no(page_no: nat) -> nat {
    page_no / segment_page_count()
}

spec fn segment_index(page_no: nat) -> nat {
    page_no % segment_page_count()
}

spec fn root_table_bytes(entry_count: nat) -> nat {
    entry_count * page_table_entry_len()
}

spec fn import_offset_fits(base: nat, offset: nat) -> bool {
    base + offset <= u64_max()
}

proof fn page_count_zero()
    ensures
        page_count_for_size(0) == 0,
{
}

proof fn page_count_within_first_page(size: nat)
    by (nonlinear_arith)
    requires
        0 < size <= sqlite_page_size(),
    ensures
        page_count_for_size(size) == 1,
{
}

proof fn segment_count_zero()
    ensures
        segment_count_for_pages(0) == 0,
{
}

proof fn segment_index_is_bounded(page_no: nat)
    by (nonlinear_arith)
    ensures
        segment_index(page_no) < segment_page_count(),
{
}

proof fn root_table_bytes_scales_by_entry_count(entry_count: nat)
    ensures
        root_table_bytes(entry_count) == entry_count * 8,
{
}

proof fn import_offset_at_u64_max_fits()
    ensures
        import_offset_fits(u64_max(), 0),
{
}

proof fn import_offset_past_u64_max_overflows()
    by (nonlinear_arith)
    ensures
        !import_offset_fits(u64_max(), 1),
{
}

}