blob: 6b8e1881f6128ddd72ae15ec956e8c068292ae42 (
plain)
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
|
#define ENTRY_COUNT 512
staload "./entry.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"
vtypedef tablePtr1(level : int) = [l : agz] (@[entry_t][ENTRY_COUNT]@l , @[entry_t][ENTRY_COUNT]@l -<lin,prf> void, uint level | ptr l)
absvt@ype table_t(level:int) = tablePtr1 level
vtypedef Table_t = [level:nat | level < 4] table_t(level)
fun table_get_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT)):<> entry_t
fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t):<!wrt> void
overload [] with table_get_at
overload [] with table_set_at
castfn consume(Table_t): void
fn get_P4() : table_t 0
fn next_table{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))
fn next_table_create{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))
|
