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
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

//! Verus model for fixed-field superblock encoding.
//!
//! The production code uses fixed-width little-endian bytes. This abstract
//! model proves the field layout is lossless and that metadata checksums ignore
//! the stored checksum field by zeroing it before hashing.

use vstd::prelude::*;

verus! {

struct Superblock {
    magic: u64,
    version: u64,
    sqlite_page_size: u64,
    db_size: u64,
    schema_version: u64,
    last_tx_id: u64,
    flags: u64,
    checksum: u64,
    import_expected_checksum: u64,
    import_written_until: u64,
    import_total_size: u64,
    import_base_offset: u64,
    checksum_refresh_offset: u64,
    checksum_refresh_hash: u64,
    checksum_refresh_tx_id: u64,
    db_base_offset: u64,
    page_table_offset: u64,
    page_count: u64,
    layout_version: u64,
    meta_checksum: u64,
}

struct EncodedSuperblock {
    fields: Seq<u64>,
}

spec fn encoded_len() -> nat {
    20
}

spec fn encode(block: Superblock) -> EncodedSuperblock {
    EncodedSuperblock {
        fields: seq![
            block.magic,
            block.version,
            block.sqlite_page_size,
            block.db_size,
            block.schema_version,
            block.last_tx_id,
            block.flags,
            block.checksum,
            block.import_expected_checksum,
            block.import_written_until,
            block.import_total_size,
            block.import_base_offset,
            block.checksum_refresh_offset,
            block.checksum_refresh_hash,
            block.checksum_refresh_tx_id,
            block.db_base_offset,
            block.page_table_offset,
            block.page_count,
            block.layout_version,
            block.meta_checksum
        ],
    }
}

spec fn decode(encoded: EncodedSuperblock) -> Superblock
    recommends
        encoded.fields.len() == encoded_len(),
{
    Superblock {
        magic: encoded.fields[0],
        version: encoded.fields[1],
        sqlite_page_size: encoded.fields[2],
        db_size: encoded.fields[3],
        schema_version: encoded.fields[4],
        last_tx_id: encoded.fields[5],
        flags: encoded.fields[6],
        checksum: encoded.fields[7],
        import_expected_checksum: encoded.fields[8],
        import_written_until: encoded.fields[9],
        import_total_size: encoded.fields[10],
        import_base_offset: encoded.fields[11],
        checksum_refresh_offset: encoded.fields[12],
        checksum_refresh_hash: encoded.fields[13],
        checksum_refresh_tx_id: encoded.fields[14],
        db_base_offset: encoded.fields[15],
        page_table_offset: encoded.fields[16],
        page_count: encoded.fields[17],
        layout_version: encoded.fields[18],
        meta_checksum: encoded.fields[19],
    }
}

spec fn zero_meta_checksum(block: Superblock) -> Superblock {
    Superblock { meta_checksum: 0, ..block }
}

spec fn meta_checksum_input(block: Superblock) -> EncodedSuperblock {
    encode(zero_meta_checksum(block))
}

proof fn encode_has_fixed_field_count(block: Superblock)
    ensures
        encode(block).fields.len() == encoded_len(),
{
    broadcast use vstd::seq::group_seq_axioms;
}

proof fn decode_encode_round_trip(block: Superblock)
    ensures
        decode(encode(block)) == block,
{
    broadcast use vstd::seq::group_seq_axioms;
    encode_has_fixed_field_count(block);
}

proof fn checksum_input_zeroes_only_meta_checksum(block: Superblock)
    ensures
        decode(meta_checksum_input(block)).meta_checksum == 0,
        decode(meta_checksum_input(block)).db_size == block.db_size,
        decode(meta_checksum_input(block)).last_tx_id == block.last_tx_id,
        decode(meta_checksum_input(block)).checksum == block.checksum,
{
    broadcast use vstd::seq::group_seq_axioms;
    encode_has_fixed_field_count(zero_meta_checksum(block));
}

}