ic-sqlite-vfs 0.2.2

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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165

//! Verus model for stable-memory capacity arithmetic.
//!
//! This proof covers the pure arithmetic behind `ensure_memory_capacity` and
//! `write_growing`: the computed extra page count is enough to contain the
//! requested end offset when checked arithmetic succeeds.

use vstd::prelude::*;

verus! {

spec fn stable_page_size() -> nat {
    65_536
}

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

spec fn checked_add(left: nat, right: nat) -> Option<nat> {
    if left + right <= u64_max() {
        Some(left + right)
    } else {
        None
    }
}

spec fn checked_mul(left: nat, right: nat) -> Option<nat> {
    if left * right <= u64_max() {
        Some(left * right)
    } else {
        None
    }
}

spec fn div_ceil(numerator: nat, denominator: nat) -> nat {
    if numerator == 0 {
        0
    } else {
        (((numerator - 1) / (denominator as int)) + 1) as nat
    }
}

spec fn extra_pages_needed(current_pages: nat, end_offset: nat) -> Option<nat> {
    match checked_mul(current_pages, stable_page_size()) {
        Some(current_bytes) => {
            if end_offset <= current_bytes {
                Some(0)
            } else {
                Some(div_ceil((end_offset - current_bytes) as nat, stable_page_size()))
            }
        },
        None => None,
    }
}

proof fn div_ceil_covers_positive(numerator: nat)
    by (nonlinear_arith)
    requires
        numerator > 0,
    ensures
        numerator <= div_ceil(numerator, stable_page_size()) * stable_page_size(),
        div_ceil(numerator, stable_page_size()) > 0,
{
}

proof fn div_ceil_zero()
    ensures
        div_ceil(0, stable_page_size()) == 0,
{
}

proof fn div_ceil_is_bounded_by_positive_numerator(numerator: nat)
    by (nonlinear_arith)
    requires
        numerator > 0,
    ensures
        div_ceil(numerator, stable_page_size()) <= numerator,
{
}

proof fn extra_pages_cover_end_offset(current_pages: nat, end_offset: nat, pages: nat)
    by (nonlinear_arith)
    requires
        extra_pages_needed(current_pages, end_offset) == Some(pages),
    ensures
        end_offset <= (current_pages + pages) * stable_page_size(),
{
    match checked_mul(current_pages, stable_page_size()) {
        Some(current_bytes) => {
            if end_offset <= current_bytes {
            } else {
                div_ceil_covers_positive((end_offset - current_bytes) as nat);
            }
        },
        None => {},
    }
}

proof fn grow_page_sum_stays_in_u64_for_u64_end(
    current_pages: nat,
    end_offset: nat,
    pages: nat,
)
    by (nonlinear_arith)
    requires
        end_offset <= u64_max(),
        extra_pages_needed(current_pages, end_offset) == Some(pages),
    ensures
        current_pages + pages <= u64_max(),
        matches!(checked_add(current_pages, pages), Some(_)),
{
    match checked_mul(current_pages, stable_page_size()) {
        Some(current_bytes) => {
            if end_offset <= current_bytes {
            } else {
                div_ceil_is_bounded_by_positive_numerator((end_offset - current_bytes) as nat);
            }
        },
        None => {},
    }
}

proof fn grow_success_capacity_covers_end_offset(
    current_pages: nat,
    end_offset: nat,
    pages: nat,
    total_pages: nat,
)
    by (nonlinear_arith)
    requires
        end_offset <= u64_max(),
        extra_pages_needed(current_pages, end_offset) == Some(pages),
        checked_add(current_pages, pages) == Some(total_pages),
    ensures
        end_offset <= total_pages * stable_page_size(),
{
    extra_pages_cover_end_offset(current_pages, end_offset, pages);
}

proof fn no_grow_needed_means_current_capacity_covers(
    current_pages: nat,
    end_offset: nat,
)
    requires
        extra_pages_needed(current_pages, end_offset) == Some(0nat),
    ensures
        end_offset <= current_pages * stable_page_size(),
{
    match checked_mul(current_pages, stable_page_size()) {
        Some(current_bytes) => {},
        None => {},
    }
}

proof fn checked_end_rejects_u64_overflow(offset: nat)
    by (nonlinear_arith)
    requires
        offset <= u64_max(),
    ensures
        checked_add(offset, (u64_max() - offset) as nat) == Some(u64_max()),
        checked_add(offset, (u64_max() - offset + 1) as nat) == Option::<nat>::None,
{
}

}