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