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