diff options
Diffstat (limited to 'kernel/memory/paging/table.sats')
| -rw-r--r-- | kernel/memory/paging/table.sats | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats index 9a103f4..491b77e 100644 --- a/kernel/memory/paging/table.sats +++ b/kernel/memory/paging/table.sats @@ -4,16 +4,24 @@ staload "./entry.sats" staload "lib/SATS/valid.sats" staload "lib/DATS/valid.dats" -typedef table_t = @[entry_t][ENTRY_COUNT] +vtypedef tablePtr1(level : int) = [l : agz] (@[entry_t][ENTRY_COUNT]@l , @[entry_t][ENTRY_COUNT]@l -<lin,prf> void, uint level | ptr l) -vtypedef tablePtr1(c : int) = @{ - ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l), - level = (uint c | ) - } +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): void +fn set_zero(&Table_t):<!wrt> void + +castfn consume(Table_t): void -fun get_P4() : tablePtr1(0) +fun get_P4() : table_t 0 -fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1)) +fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) |