#define ENTRY_COUNT 512

staload "./entry.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"

typedef table_t = @[entry_t][ENTRY_COUNT]

vtypedef tablePtr1(c : int)  = @{
    ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l),
    level = (uint c | )
  }

// Set all the entries in the table to unused (zero)
fn set_zero(&table_t): void

fun get_P4() : tablePtr1(0)

fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1))