ic-sqlite-vfs 1.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

//! Verus model for MemoryManager allocation-table invariants.
//!
//! The production loader rejects allocated buckets without an owner, unallocated
//! buckets with an owner, and memory size / bucket count mismatches.

use vstd::prelude::*;

verus! {

spec fn max_num_memories() -> nat {
    255
}

spec fn max_num_buckets() -> nat {
    32_768
}

spec fn unallocated_marker() -> nat {
    max_num_memories()
}

spec fn bucket_size_in_pages() -> nat {
    128
}

spec fn bucket_count_for_pages(pages: nat) -> nat {
    if pages == 0 {
        0
    } else {
        (((pages - 1) / (bucket_size_in_pages() as int)) + 1) as nat
    }
}

spec fn allocated_owner_valid(bucket: nat, allocated_buckets: nat, owner: nat) -> bool {
    bucket < allocated_buckets ==> owner < max_num_memories()
}

spec fn unallocated_owner_valid(bucket: nat, allocated_buckets: nat, owner: nat) -> bool {
    allocated_buckets <= bucket < max_num_buckets() ==> owner == unallocated_marker()
}

spec fn memory_size_matches_bucket_count(size_pages: nat, bucket_count: nat) -> bool {
    bucket_count_for_pages(size_pages) == bucket_count
}

proof fn allocated_bucket_owner_is_memory_id(bucket: nat, allocated_buckets: nat, owner: nat)
    requires
        bucket < allocated_buckets,
        allocated_owner_valid(bucket, allocated_buckets, owner),
    ensures
        owner < max_num_memories(),
{
}

proof fn unallocated_bucket_uses_marker(bucket: nat, allocated_buckets: nat, owner: nat)
    requires
        allocated_buckets <= bucket < max_num_buckets(),
        unallocated_owner_valid(bucket, allocated_buckets, owner),
    ensures
        owner == unallocated_marker(),
{
}

proof fn bucket_count_covers_memory_size(size_pages: nat)
    by (nonlinear_arith)
    ensures
        size_pages <= bucket_count_for_pages(size_pages) * bucket_size_in_pages(),
{
}

proof fn matching_memory_size_has_expected_bucket_count(size_pages: nat, bucket_count: nat)
    requires
        memory_size_matches_bucket_count(size_pages, bucket_count),
    ensures
        bucket_count == bucket_count_for_pages(size_pages),
{
}

proof fn allocated_bucket_count_is_within_table(allocated_buckets: nat)
    requires
        allocated_buckets <= max_num_buckets(),
    ensures
        allocated_buckets <= 32_768,
{
}

}