blob: 491b77eef40cec1166f5483078d5875a515426bb (
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
27
|
#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
// Set all the entries in the table to unused (zero)
fn set_zero(&Table_t):<!wrt> void
castfn consume(Table_t): void
fun get_P4() : table_t 0
fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))
|
