| symbol | specification | entry |
|---|
| # | address-list-set | function,
address-set → nat |
| # | address-list-set | function,
address-list → nat |
| # | node-store | function,
address-set → nat |
| # | node-store | function,
node-store → nat |
| # | node-index | function,
key-set → nat |
| # | node-index | function,
node-index → nat |
| # | set-basic | function,
set → nat |
| # | store | function,
store → nat |
| # | array | function,
array → nat |
| # | list-data | function,
list → nat |
| # | buffer | function,
buffer → nat |
| # | nat-list-set | function,
nat-set → nat |
| # | nat-list-set | function,
nat-list → nat |
| # | group-store | function,
group-address-store → nat |
| # | group-store | function,
group-store → nat |
| # | group-store | function,
group-node-list → nat |
| # | index-store | function,
index-address-store → nat |
| # | index-store | function,
index-store → nat |
| # | index-store | function,
index-node-list → nat |
| # | stringset | function,
stringset → nat |
| # | nat-store | function,
nat-set → nat |
| # | nat-set | function,
nat-set → nat |
| # | key-list-set | function,
key-set → nat |
| # | key-list-set | function,
key-list → nat |
| # | laddress-list | function,
laddress-list → nat |
| # | branch-array | function,
branch-array → nat |
| # | address-store | function,
address-set → nat |
| # | address-store | function,
address-store → nat |
| # | node-list | function,
node-list → nat |
| # | string | function,
string → nat |
| % | nat-div | partial function,
nat × nat → nat |
| ' | address-list-set | function,
address → address-list |
| ' | list | function,
elem → list |
| ' | nat-list-set | function,
nat → nat-list |
| ' | group-store | function,
group-node → group-node-list |
| ' | index-store | function,
index-node → index-node-list |
| ' | key-list-set | function,
key → key-list |
| ' | laddress-list | function,
laddress → laddress-list |
| ' | node-list | function,
node → node-list |
| ' | string | function,
char → string |
| * | nat-mult | function,
nat × nat → nat |
| + | address-list-set | function,
address-list × address → address-list |
| + | address-list-set | function,
address-list × address-list → address-list |
| + | address-list-set | function,
address × address-list → address-list |
| + | array-splice | function,
array × array → array |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → list |
| + | list-data | function,
elem × list → list |
| + | buffer | function,
buffer × buffer → buffer |
| + | nat-list-set | function,
nat-list × nat → nat-list |
| + | nat-list-set | function,
nat-list × nat-list → nat-list |
| + | nat-list-set | function,
nat × nat-list → nat-list |
| + | group-store | function,
group-node-list × group-node → group-node-list |
| + | group-store | function,
group-node-list × group-node-list → group-node-list |
| + | group-store | function,
group-node × group-node-list → group-node-list |
| + | index-store | function,
index-node-list × index-node → index-node-list |
| + | index-store | function,
index-node-list × index-node-list → index-node-list |
| + | index-store | function,
index-node × index-node-list → index-node-list |
| + | key-list-set | function,
key-list × key → key-list |
| + | key-list-set | function,
key-list × key-list → key-list |
| + | key-list-set | function,
key × key-list → key-list |
| + | laddress-list | function,
laddress-list × laddress → laddress-list |
| + | laddress-list | function,
laddress-list × laddress-list → laddress-list |
| + | laddress-list | function,
laddress × laddress-list → laddress-list |
| + | node-list | function,
node-list × node → node-list |
| + | node-list | function,
node-list × node-list → node-list |
| + | node-list | function,
node × node-list → node-list |
| + | nat-basic | function,
nat × nat → nat |
| + | string | function,
string × char → string |
| + | string | function,
string × string → string |
| + | string | function,
char × string → string |
| ++ | address-list-set | function,
address-set × address → address-set |
| ++ | address-list-set | function,
address-list × address → address-list |
| ++ | node-store | function,
address-set × address → address-set |
| ++ | node-index | function,
key-set × key → key-set |
| ++ | set-basic | function,
set × elem → set |
| ++ | list-dup | function,
list × elem → list |
| ++ | nat-list-set | function,
nat-set × nat → nat-set |
| ++ | nat-list-set | function,
nat-list × nat → nat-list |
| ++ | group-store | function,
group-node-list × group-node → group-node-list |
| ++ | index-store | function,
index-node-list × index-node → index-node-list |
| ++ | stringset | function,
stringset × string → stringset |
| ++ | nat-store | function,
nat-set × nat → nat-set |
| ++ | nat-set | function,
nat-set × nat → nat-set |
| ++ | key-list-set | function,
key-set × key → key-set |
| ++ | key-list-set | function,
key-list × key → key-list |
| ++ | laddress-list | function,
laddress-list × laddress → laddress-list |
| ++ | address-store | function,
address-set × address → address-set |
| ++ | node-list | function,
node-list × node → node-list |
| ++ | string | function,
string × char → string |
| +1 | nat-basic | function,
nat → nat |
| +2 | address-list-set | function,
address × address → address-list |
| +2 | list | function,
elem × elem → list |
| +2 | nat-list-set | function,
nat × nat → nat-list |
| +2 | group-store | function,
group-node × group-node → group-node-list |
| +2 | index-store | function,
index-node × index-node → index-node-list |
| +2 | key-list-set | function,
key × key → key-list |
| +2 | laddress-list | function,
laddress × laddress → laddress-list |
| +2 | node-list | function,
node × node → node-list |
| +2 | string | function,
char × char → string |
| - | nat | partial function,
nat × nat → nat |
| -- | address-list-set | function,
address-set × address → address-set |
| -- | node-store | function,
address-set × address → address-set |
| -- | node-store | function,
node-store × address → node-store |
| -- | node-index | function,
key-set × key → key-set |
| -- | node-index | function,
node-index × key → node-index |
| -- | set-union | function,
set × elem → set |
| -- | store | function,
store × elem → store |
| -- | nat-list-set | function,
nat-set × nat → nat-set |
| -- | group-store | function,
group-address-store × address → group-address-store |
| -- | group-store | function,
group-store × nat → group-store |
| -- | index-store | function,
index-address-store × address → index-address-store |
| -- | index-store | function,
index-store × nat → index-store |
| -- | stringset | function,
stringset × string → stringset |
| -- | nat-store | function,
nat-set × nat → nat-set |
| -- | nat-store | function,
store × nat → store |
| -- | nat-set | function,
nat-set × nat → nat-set |
| -- | key-list-set | function,
key-set × key → key-set |
| -- | address-store | function,
address-set × address → address-set |
| -- | address-store | function,
address-store × address → address-store |
| -1 | nat-basic | partial function,
nat → nat |
| -1l | address-list-set | function,
address-list × address → address-list |
| -1l | list-del | function,
list × elem → list |
| -1l | nat-list-set | function,
nat-list × nat → nat-list |
| -1l | group-store | function,
group-node-list × group-node → group-node-list |
| -1l | index-store | function,
index-node-list × index-node → index-node-list |
| -1l | key-list-set | function,
key-list × key → key-list |
| -1l | laddress-list | function,
laddress-list × laddress → laddress-list |
| -1l | node-list | function,
node-list × node → node-list |
| -1l | string | function,
string × char → string |
| -l | address-list-set | function,
address-list × address → address-list |
| -l | list-del | function,
list × elem → list |
| -l | nat-list-set | function,
nat-list × nat → nat-list |
| -l | group-store | function,
group-node-list × group-node → group-node-list |
| -l | index-store | function,
index-node-list × index-node → index-node-list |
| -l | key-list-set | function,
key-list × key → key-list |
| -l | laddress-list | function,
laddress-list × laddress → laddress-list |
| -l | node-list | function,
node-list × node → node-list |
| -l | string | function,
string × char → string |
| -p | address-list-set | function,
address-list × nat → address-list |
| -p | list-del | function,
list × nat → list |
| -p | nat-list-set | function,
nat-list × nat → nat-list |
| -p | group-store | function,
group-node-list × nat → group-node-list |
| -p | index-store | function,
index-node-list × nat → index-node-list |
| -p | key-list-set | function,
key-list × nat → key-list |
| -p | laddress-list | function,
laddress-list × nat → laddress-list |
| -p | node-list | function,
node-list × nat → node-list |
| -p | string | function,
string × nat → string |
| .adr | branch | function,
branch → address |
| .adr:= | branch | function,
branch × address → branch |
| .branch? | branch | predicate,
branch |
| .branches | indexnode | function,
index-node → branch-array |
| .branches:= | indexnode | function,
index-node × branch-array → index-node |
| .butlast | address-list-set | partial function,
address-list → address-list |
| .butlast | list-last | partial function,
list → list |
| .butlast | nat-list-set | partial function,
nat-list → nat-list |
| .butlast | group-store | partial function,
group-node-list → group-node-list |
| .butlast | index-store | partial function,
index-node-list → index-node-list |
| .butlast | key-list-set | partial function,
key-list → key-list |
| .butlast | laddress-list | partial function,
laddress-list → laddress-list |
| .butlast | node-list | partial function,
node-list → node-list |
| .butlast | string | partial function,
string → string |
| .butmax | oset | partial function,
set → set |
| .butmax | nat-set | partial function,
nat-set → nat-set |
| .butmin | oset | partial function,
set → set |
| .butmin | nat-set | partial function,
nat-set → nat-set |
| .char1 | string | partial function,
string → char |
| .data | node | partial function,
node → buffer |
| .data:= | node | partial function,
node × buffer → node |
| .data? | node | predicate,
node |
| .data? | key | predicate,
key |
| .dentry? | node | predicate,
node |
| .dentry? | dentry | predicate,
dentry |
| .dentry? | key | predicate,
key |
| .directory | node | partial predicate,
node |
| .directory | inode | predicate,
inode |
| .directory:= | node | partial function,
node × bool → node |
| .directory:= | inode | function,
inode × bool → inode |
| .end | groupnode | predicate,
group-node |
| .end:= | groupnode | function,
group-node × bool → group-node |
| .entry? | branch | predicate,
branch |
| .flashsize | group-store | function,
group-node-list → nat |
| .flashsize | group-store | function,
group-node → nat |
| .flashsize | index-store | function,
index-node-list → nat |
| .flashsize | index-store | function,
index-node → nat |
| .flashsize | ablock-store-inv | function,
list → nat |
| .flashsize | ablock-store-inv | function,
elem → nat |
| .flashsize | gjournal-base | function,
node-list → nat |
| .flashsize | gjournal-base | function,
node → nat |
| .gndlist | group-store | function,
group-block → group-node-list |
| .gndlist:= | group-store | function,
group-block × group-node-list → group-block |
| .head | address-list-set | partial function,
address-list → address |
| .head | list-data | partial function,
list → elem |
| .head | nat-list-set | partial function,
nat-list → nat |
| .head | group-store | partial function,
group-node-list → group-node |
| .head | index-store | partial function,
index-node-list → index-node |
| .head | key-list-set | partial function,
key-list → key |
| .head | laddress-list | partial function,
laddress-list → laddress |
| .head | node-list | partial function,
node-list → node |
| .index? | persistence-state | predicate,
persistence-state |
| .indlist | index-store | function,
index-block → index-node-list |
| .indlist:= | index-store | function,
index-block × index-node-list → index-block |
| .ino | node | partial function,
node → nat |
| .ino | inode | function,
inode → nat |
| .ino | dentry | partial function,
dentry → nat |
| .ino | key | function,
key → nat |
| .ino:= | node | partial function,
node × nat → node |
| .ino:= | inode | function,
inode × nat → inode |
| .ino:= | dentry | partial function,
dentry × nat → dentry |
| .ino:= | key | function,
key × nat → key |
| .inode? | node | predicate,
node |
| .inode? | key | predicate,
key |
| .inodes? | aubifs-inv | predicate,
key-set |
| .inos | gjournal-base | function,
node-index → nat-set |
| .journal? | persistence-state | predicate,
persistence-state |
| .key | node | function,
node → key |
| .key | branch | function,
branch → key |
| .key:= | node | function,
node × key → node |
| .key:= | branch | function,
branch × key → branch |
| .keys | gjournal-base | function,
node-list → key-list |
| .keys | gjournal-base | function,
nat-set → key-set |
| .ladrlist | group-store | function,
group-block → laddress-list |
| .ladrlist | index-store | function,
index-block → laddress-list |
| .ladrlist | ablock | function,
ablock → laddress-list |
| .ladrlist:= | group-store | function,
group-block × laddress-list → group-block |
| .ladrlist:= | index-store | function,
index-block × laddress-list → index-block |
| .ladrlist:= | ablock | function,
ablock × laddress-list → ablock |
| .last | address-list-set | partial function,
address-list → address |
| .last | list-last | partial function,
list → elem |
| .last | nat-list-set | partial function,
nat-list → nat |
| .last | group-store | partial function,
group-node-list → group-node |
| .last | index-store | partial function,
index-node-list → index-node |
| .last | key-list-set | partial function,
key-list → key |
| .last | laddress-list | partial function,
laddress-list → laddress |
| .last | node-list | partial function,
node-list → node |
| .last | string | partial function,
string → char |
| .leaf | indexnode | predicate,
index-node |
| .leaf:= | indexnode | function,
index-node × bool → index-node |
| .lebs | gjournal-base | function,
address-set → nat-set |
| .lebs | gjournal-base | function,
address-list → nat-set |
| .lebs | gjournal-base | function,
node-index → nat-set |
| .list | ablock | function,
ablock → list |
| .list:= | ablock | function,
ablock × list → ablock |
| .lnum | address-data | function,
address → nat |
| .lnum | persistence-state | partial function,
persistence-state → nat |
| .lnum:= | address-data | function,
address × nat → address |
| .map | group-store | function,
group-address-store × address × group-node → group-node → group-address-store |
| .map | group-store | function,
group-address-store × group-node → group-node → group-address-store |
| .map | group-store | function,
group-store × nat × group-block → group-block → group-store |
| .map | group-store | function,
group-store × group-block → group-block → group-store |
| .map | index-store | function,
index-address-store × address × index-node → index-node → index-address-store |
| .map | index-store | function,
index-address-store × index-node → index-node → index-address-store |
| .map | index-store | function,
index-store × nat × index-block → index-block → index-store |
| .map | index-store | function,
index-store × index-block → index-block → index-store |
| .map | nat-store | function,
store × nat × data → data → store |
| .map | ablock-store | function,
store × nat × ablock → ablock → store |
| .map | ablock-store | function,
store × ablock → ablock → store |
| .map | store-map | function,
store × elem × data → data → store |
| .map | store-map | function,
store × data → data → store |
| .map | address-store | function,
address-store × address × elem → elem → address-store |
| .map | address-store | function,
address-store × elem → elem → address-store |
| .max | oset | partial function,
set → elem |
| .max | nat-set | partial function,
nat-set → nat |
| .meta | node | partial function,
node → metadata |
| .meta | inode | function,
inode → metadata |
| .meta:= | node | partial function,
node × metadata → node |
| .meta:= | inode | function,
inode × metadata → inode |
| .min | oset | partial function,
set → elem |
| .min | nat-set | partial function,
nat-set → nat |
| .name | dentry | function,
dentry → string |
| .name | key | partial function,
key → string |
| .name:= | dentry | function,
dentry × string → dentry |
| .name:= | key | partial function,
key × string → key |
| .nd | groupnode | function,
group-node → node |
| .nd:= | groupnode | function,
group-node × node → group-node |
| .nds | gjournal-base | function,
group-node-list → node-list |
| .negdentry? | dentry | predicate,
dentry |
| .nlink | node | partial function,
node → nat |
| .nlink | inode | function,
inode → nat |
| .nlink:= | node | partial function,
node × nat → node |
| .nlink:= | inode | function,
inode × nat → inode |
| .nsubdirs | node | partial function,
node → nat |
| .nsubdirs | inode | function,
inode → nat |
| .nsubdirs:= | node | partial function,
node × nat → node |
| .nsubdirs:= | inode | function,
inode × nat → inode |
| .off | laddress | function,
laddress → nat |
| .off:= | laddress | function,
laddress × nat → laddress |
| .part | key | partial function,
key → nat |
| .part:= | key | partial function,
key × nat → key |
| .pos | address-data | function,
address → nat |
| .pos:= | address-data | function,
address × nat → address |
| .ref-size | group-store | function,
group-block → nat |
| .ref-size | index-store | function,
index-block → nat |
| .ref-size | ablock | function,
ablock → nat |
| .ref-size:= | group-store | function,
group-block × nat → group-block |
| .ref-size:= | index-store | function,
index-block × nat → index-block |
| .ref-size:= | ablock | function,
ablock × nat → ablock |
| .rstring | string | partial function,
string → string |
| .size | node | partial function,
node → nat |
| .size | address-data | function,
address → nat |
| .size | inode | function,
inode → nat |
| .size | laddress | function,
laddress → nat |
| .size | ablock-store-refsize-cons | function,
address-set → nat |
| .size:= | node | partial function,
node × nat → node |
| .size:= | address-data | function,
address × nat → address |
| .size:= | inode | function,
inode × nat → inode |
| .size:= | laddress | function,
laddress × nat → laddress |
| .sqnum | groupnode | function,
group-node → nat |
| .sqnum:= | groupnode | function,
group-node × nat → group-node |
| .start | groupnode | predicate,
group-node |
| .start:= | groupnode | function,
group-node × bool → group-node |
| .tail | address-list-set | partial function,
address-list → address-list |
| .tail | list-data | partial function,
list → list |
| .tail | nat-list-set | partial function,
nat-list → nat-list |
| .tail | group-store | partial function,
group-node-list → group-node-list |
| .tail | index-store | partial function,
index-node-list → index-node-list |
| .tail | key-list-set | partial function,
key-list → key-list |
| .tail | laddress-list | partial function,
laddress-list → laddress-list |
| .tail | node-list | partial function,
node-list → node-list |
| .to-adr | ablock-store-inv | function,
laddress-list × nat → address-list |
| .toSet | address-list-set | function,
address-list → address-set |
| .toSet | nat-list-set | function,
nat-list → nat-set |
| .toSet | key-list-set | function,
key-list → key-set |
| .toSet | list+set | function,
list → set |
| .toString | debug | function,
nat → string |
| .trunc? | node | predicate,
node |
| .usedsize | indexnode | function,
index-node → nat |
| .usedsize:= | indexnode | function,
index-node × nat → index-node |
| / | nat-div | partial function,
nat × nat → nat |
| < | address-list-set | predicate,
address-list × address-list |
| < | list-data | predicate,
list × list |
| < | nat-list-set | predicate,
nat-list × nat-list |
| < | group-store | predicate,
group-node-list × group-node-list |
| < | index-store | predicate,
index-node-list × index-node-list |
| < | oelem | predicate,
elem × elem |
| < | oset | predicate,
set × elem |
| < | oset | predicate,
elem × set |
| < | nat-set | predicate,
nat-set × nat |
| < | nat-set | predicate,
nat × nat-set |
| < | key-list-set | predicate,
key-list × key-list |
| < | laddress-list | predicate,
laddress-list × laddress-list |
| < | node-list | predicate,
node-list × node-list |
| < | nat-basic | predicate,
nat × nat |
| =○refsize | group-store | predicate,
group-store × group-store |
| =○refsize | index-store | predicate,
index-store × index-store |
| =○refsize | ablock-store-inv | predicate,
store × store |
| > | nat | predicate,
nat × nat |
| @ | address-data | function,
nat × nat × nat → address |
| @ | laddress | function,
nat × nat → laddress |
| ADR | index-asm | variable,
address,flexible |
| ADR | aubifs-internal-asm | variable,
address,flexible |
| ADR0 | gjournal-asm | variable,
address,flexible |
| ADR0 | aubifs-internal-asm | variable,
address,flexible |
| ADR1 | gjournal-asm | variable,
address,flexible |
| ADR1 | aubifs-internal-asm | variable,
address,flexible |
| ADR2 | gjournal-asm | variable,
address,flexible |
| ADR2 | aubifs-internal-asm | variable,
address,flexible |
| ADR3 | gjournal-asm | variable,
address,flexible |
| ADR3 | aubifs-internal-asm | variable,
address,flexible |
| ADR4 | gjournal-asm | variable,
address,flexible |
| ADR4 | aubifs-internal-asm | variable,
address,flexible |
| ADR5 | gjournal-asm | variable,
address,flexible |
| ADR5 | aubifs-internal-asm | variable,
address,flexible |
| ADRLIST | index-asm | variable,
address-list,flexible |
| ADRLIST0 | gjournal-asm | variable,
address-list,flexible |
| ADRLIST1 | gjournal-asm | variable,
address-list,flexible |
| ADR_DUMMY | constants | constant,
address |
| AS | index-asm | variable,
address-set,flexible |
| AS | aubifs-internal-asm | variable,
address-set,flexible |
| AX | aubifs-internal-asm | variable,
address-list,flexible |
| AX0 | aubifs-internal-asm | variable,
address-list,flexible |
| AX1 | aubifs-internal-asm | variable,
address-list,flexible |
| BRANCH_SIZE | constants | constant,
nat |
| COMMIT? | index-asm | variable,
bool,flexible |
| CSYNCED | aubifs-internal-asm | variable,
bool,flexible |
| DONE | gjournal-asm | variable,
bool,flexible |
| DOSYNC | gjournal-asm | variable,
bool,flexible |
| DOSYNC | aubifs-internal-asm | variable,
bool,flexible |
| DOSYNC0 | gjournal-asm | variable,
bool,flexible |
| DOSYNC0 | aubifs-internal-asm | variable,
bool,flexible |
| EACCESS | error | constant,
error |
| EBADFD | error | constant,
error |
| EB_PAGE_SIZE | eraseblock | constant,
nat |
| ECOMMIT | error | constant,
error |
| EEXISTS | error | constant,
error |
| EFAIL | error | constant,
error |
| EINVAL | error | constant,
error |
| EIO | error | constant,
error |
| EISDIR | error | constant,
error |
| EMPTY? | index-asm | variable,
bool,flexible |
| ENOENT | error | constant,
error |
| ENOMEM | error | constant,
error |
| ENOSPC | error | constant,
error |
| ENOTDIR | error | constant,
error |
| ENOTEMPTY | error | constant,
error |
| EROFS | error | constant,
error |
| ERR | error-class | variable,
error,flexible |
| ERR0 | error-class | variable,
error,flexible |
| ESUCCESS | error | constant,
error |
| EUCLEAN | error | constant,
error |
| EXISTS | index-asm | variable,
bool,flexible |
| EXISTS | aubifs-internal-asm | variable,
bool,flexible |
| FI | aubifs-internal-asm | variable,
node-index,flexible |
| FIRST? | gjournal-asm | variable,
bool,flexible |
| FO | aubifs-internal-asm | variable,
key-set,flexible |
| FS | aubifs-internal-asm | variable,
node-store,flexible |
| GND | index-asm | variable,
group-node,flexible |
| GND0 | gjournal-asm | variable,
group-node,flexible |
| GND1 | gjournal-asm | variable,
group-node,flexible |
| GND2 | gjournal-asm | variable,
group-node,flexible |
| GND3 | gjournal-asm | variable,
group-node,flexible |
| GND4 | gjournal-asm | variable,
group-node,flexible |
| GNDLIST | index-asm | variable,
group-node-list,flexible |
| GNDLIST1 | gjournal-asm | variable,
group-node-list,flexible |
| GROUP_NODE_HEADER_SIZE | gjournal-base | constant,
nat |
| IND | index-asm | variable,
index-node,flexible |
| ISYNCED | index-asm | variable,
bool,flexible |
| JGINVAL | gjournal-asm | variable,
nat-set,flexible |
| JMAXINO | gjournal-asm | variable,
nat,flexible |
| JNL | gjournal-asm | variable,
nat-list,flexible |
| JRO | gjournal-asm | variable,
nat-set,flexible |
| JRO0 | gjournal-asm | variable,
nat-set,flexible |
| JVALID | gjournal-asm | variable,
bool,flexible |
| KEY | index-asm | variable,
key,flexible |
| KEY | aubifs-internal-asm | variable,
key,flexible |
| KEY0 | aubifs-internal-asm | variable,
key,flexible |
| KEY1 | aubifs-internal-asm | variable,
key,flexible |
| KEY2 | aubifs-internal-asm | variable,
key,flexible |
| KEY3 | aubifs-internal-asm | variable,
key,flexible |
| KEY4 | aubifs-internal-asm | variable,
key,flexible |
| KEY5 | aubifs-internal-asm | variable,
key,flexible |
| KEYLIST | gjournal-asm | variable,
key-list,flexible |
| KS | index-asm | variable,
key-set,flexible |
| KS | aubifs-internal-asm | variable,
key-set,flexible |
| KX | aubifs-internal-asm | variable,
key-list,flexible |
| LADR | index-asm | variable,
laddress,flexible |
| LADRLIST | index-asm | variable,
laddress-list,flexible |
| LAST? | gjournal-asm | variable,
bool,flexible |
| LEB_SIZE | eraseblock | constant,
nat |
| LNUM | index-asm | variable,
nat,flexible |
| LOG | gjournal-asm | variable,
address-list,flexible |
| LOG | aubifs-internal-asm | variable,
address-list,flexible |
| MIN_SIZE | constants | constant,
nat |
| N | index-asm | variable,
nat,flexible |
| N | aubifs-internal-asm | variable,
nat,flexible |
| N0 | index-asm | variable,
nat,flexible |
| NAMES | index-asm | variable,
stringset,flexible |
| NAMES | aubifs-internal-asm | variable,
stringset,flexible |
| ND | index-asm | variable,
node,flexible |
| ND | aubifs-internal-asm | variable,
node,flexible |
| ND0 | gjournal-asm | variable,
node,flexible |
| ND0 | aubifs-internal-asm | variable,
node,flexible |
| ND1 | gjournal-asm | variable,
node,flexible |
| ND1 | aubifs-internal-asm | variable,
node,flexible |
| ND2 | gjournal-asm | variable,
node,flexible |
| ND2 | aubifs-internal-asm | variable,
node,flexible |
| ND3 | gjournal-asm | variable,
node,flexible |
| ND3 | aubifs-internal-asm | variable,
node,flexible |
| ND4 | gjournal-asm | variable,
node,flexible |
| ND4 | aubifs-internal-asm | variable,
node,flexible |
| ND5 | gjournal-asm | variable,
node,flexible |
| ND5 | aubifs-internal-asm | variable,
node,flexible |
| NDLIST | gjournal-asm | variable,
node-list,flexible |
| NDLIST0 | gjournal-asm | variable,
node-list,flexible |
| NS | index-asm | variable,
nat-set,flexible |
| NS0 | index-asm | variable,
nat-set,flexible |
| NS1 | index-asm | variable,
nat-set,flexible |
| OLDADR | index-asm | variable,
address,flexible |
| PAGES_PER_LEB | eraseblock | constant,
nat |
| PAGES_PER_PEB | eraseblock | constant,
nat |
| PEB_SIZE | eraseblock | constant,
nat |
| PFI | index-asm | variable,
node-index,flexible |
| PINVAL | index-asm | variable,
nat-set,flexible |
| PMAXINO | index-asm | variable,
nat,flexible |
| PMAXINO0 | index-asm | variable,
nat,flexible |
| PNL | index-asm | variable,
nat-list,flexible |
| PNL0 | index-asm | variable,
nat-list,flexible |
| PPMAXINO | index-asm | variable,
nat,flexible |
| PPMAXINO0 | index-asm | variable,
nat,flexible |
| PRI | index-asm | variable,
node-index,flexible |
| PSTORE | index-asm | variable,
group-store,flexible |
| PSTORE0 | index-asm | variable,
group-store,flexible |
| P_OS | index-asm | variable,
nat-set,flexible |
| P_OS0 | index-asm | variable,
nat-set,flexible |
| RI | aubifs-internal-asm | variable,
node-index,flexible |
| RO | aubifs-internal-asm | variable,
key-set,flexible |
| ROOT_INO | root-ino | constant,
nat |
| SIZE | index-asm | variable,
nat,flexible |
| SIZE | aubifs-internal-asm | variable,
nat,flexible |
| SIZE0 | gjournal-asm | variable,
nat,flexible |
| SIZE1 | gjournal-asm | variable,
nat,flexible |
| SIZE2 | gjournal-asm | variable,
nat,flexible |
| SIZE3 | gjournal-asm | variable,
nat,flexible |
| SIZE4 | gjournal-asm | variable,
nat,flexible |
| SQNUM | gjournal-asm | variable,
nat,flexible |
| VFS_PAGE_SIZE | page | constant,
nat |
| VOLSIZE | index-asm | variable,
nat,flexible |
| VOLSIZE | aubifs-internal-asm | variable,
nat,flexible |
| [] | address-list-set | constant,
address-list |
| [] | list-data | constant,
list |
| [] | nat-list-set | constant,
nat-list |
| [] | group-store | constant,
group-node-list |
| [] | index-store | constant,
index-node-list |
| [] | key-list-set | constant,
key-list |
| [] | laddress-list | constant,
laddress-list |
| [] | node-list | constant,
node-list |
| \ | address-list-set | function,
address-set × address-set → address-set |
| \ | node-store | function,
node-store × address-set → node-store |
| \ | node-store | function,
address-set × address-set → address-set |
| \ | node-index | function,
node-index × key-set → node-index |
| \ | node-index | function,
key-set × key-set → key-set |
| \ | store+set | function,
store × set → store |
| \ | set-union | function,
set × set → set |
| \ | nat-list-set | function,
nat-set × nat-set → nat-set |
| \ | group-store | function,
group-address-store × address-set → group-address-store |
| \ | group-store | function,
group-store × nat-set → group-store |
| \ | index-store | function,
index-address-store × address-set → index-address-store |
| \ | index-store | function,
index-store × nat-set → index-store |
| \ | stringset | function,
stringset × stringset → stringset |
| \ | nat-store | function,
store × nat-set → store |
| \ | nat-store | function,
nat-set × nat-set → nat-set |
| \ | nat-set | function,
nat-set × nat-set → nat-set |
| \ | key-list-set | function,
key-set × key-set → key-set |
| \ | address-store | function,
address-store × address-set → address-store |
| \ | address-store | function,
address-set × address-set → address-set |
| ] | address-list-set | partial function,
address-list × nat × address → address-list |
| ] | address-list-set | partial function,
address-list × nat → address |
| ] | node-store | partial function,
node-store × address → node |
| ] | node-store | function,
node-store × address × node → node-store |
| ] | node-index | partial function,
node-index × key → address |
| ] | node-index | function,
node-index × key × address → node-index |
| ] | store | partial function,
store × elem → data |
| ] | store | function,
store × elem × data → store |
| ] | array | partial function,
array × nat × elem → array |
| ] | array | partial function,
array × nat → elem |
| ] | list-del | partial function,
list × nat × elem → list |
| ] | list-del | partial function,
list × nat → elem |
| ] | buffer | partial function,
buffer × nat × data → buffer |
| ] | buffer | partial function,
buffer × nat → data |
| ] | nat-list-set | partial function,
nat-list × nat × nat → nat-list |
| ] | nat-list-set | partial function,
nat-list × nat → nat |
| ] | group-store | partial function,
group-address-store × address → group-node |
| ] | group-store | partial function,
group-store × nat → group-block |
| ] | group-store | partial function,
group-node-list × nat × group-node → group-node-list |
| ] | group-store | partial function,
group-node-list × nat → group-node |
| ] | group-store | function,
group-address-store × address × group-node → group-address-store |
| ] | group-store | function,
group-store × address → group-node |
| ] | group-store | function,
group-store × nat × group-block → group-store |
| ] | index-store | partial function,
index-address-store × address → index-node |
| ] | index-store | partial function,
index-store × nat → index-block |
| ] | index-store | partial function,
index-node-list × nat × index-node → index-node-list |
| ] | index-store | partial function,
index-node-list × nat → index-node |
| ] | index-store | function,
index-address-store × address × index-node → index-address-store |
| ] | index-store | function,
index-store × address → index-node |
| ] | index-store | function,
index-store × nat × index-block → index-store |
| ] | nat-store | partial function,
store × nat → data |
| ] | nat-store | function,
store × nat × data → store |
| ] | ablock-store | partial function,
store × nat → ablock |
| ] | ablock-store | function,
store × nat × ablock → store |
| ] | ablock-store-inv | function,
store × address → elem |
| ] | key-list-set | partial function,
key-list × nat × key → key-list |
| ] | key-list-set | partial function,
key-list × nat → key |
| ] | laddress-list | partial function,
laddress-list × nat × laddress → laddress-list |
| ] | laddress-list | partial function,
laddress-list × nat → laddress |
| ] | branch-array | partial function,
branch-array × nat × branch → branch-array |
| ] | branch-array | partial function,
branch-array × nat → branch |
| ] | index-base | function,
node-index × key-set → address-set |
| ] | address-store | partial function,
address-store × address → elem |
| ] | address-store | function,
address-store × address × elem → address-store |
| ] | aubifs-base | function,
node-store × address-list → node-list |
| ] | aubifs-base | function,
node-store × address-list × node-list → node-store |
| ] | aubifs-base | function,
node-index × key-list → address-list |
| ] | aubifs-base | function,
node-index × key-list × address-list → node-index |
| ] | node-list | partial function,
node-list × nat × node → node-list |
| ] | node-list | partial function,
node-list × nat → node |
| ] | string | partial function,
string × nat × char → string |
| ] | string | partial function,
string × nat → char |
| a | elem | variable,
elem |
| a0 | list-data | variable,
elem |
| a0 | address-store | variable,
elem |
| ablock | ablock | variable,
ablock |
| ablock | ablock | sort,
|
| ablock0 | ablock-store | variable,
ablock |
| ablock1 | ablock-store | variable,
ablock |
| ablock2 | ablock-store | variable,
ablock |
| abs-log | gjournal-abs | function,
nat-list × group-store → address-list |
| address | address | sort,
|
| address | address-data | sort,
|
| address-list | address-list-set | sort,
|
| address-set | address-list-set | sort,
|
| address-set | node-store | sort,
|
| address-set | address-store | sort,
|
| address-store | address-store | sort,
|
| addresselemf | address-store | variable,
address × elem → elem |
| addressgf | group-store | variable,
address × group-node → group-node |
| addressif | index-store | variable,
address × index-node → index-node |
| adr | address | variable,
address |
| adr | address-data | variable,
address |
| adr0 | address | variable,
address |
| adr1 | address | variable,
address |
| adr1 | address-store | variable,
address |
| adr2 | address | variable,
address |
| adr2 | address-store | variable,
address |
| adr3 | address | variable,
address |
| adr4 | address | variable,
address |
| adr5 | address | variable,
address |
| align↑ | align | function,
nat × nat → nat |
| align↓ | align | function,
nat × nat → nat |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| as | address-list-set | variable,
address-set |
| as | node-store | variable,
address-set |
| as | address-store | variable,
address-set |
| as0 | address-list-set | variable,
address-set |
| as0 | node-store | variable,
address-set |
| as0 | address-store | variable,
address-set |
| as1 | address-list-set | variable,
address-set |
| as1 | node-store | variable,
address-set |
| as1 | address-store | variable,
address-set |
| as2 | address-list-set | variable,
address-set |
| as2 | node-store | variable,
address-set |
| as2 | address-store | variable,
address-set |
| ast | address-store | variable,
address-store |
| ast0 | address-store | variable,
address-store |
| ast1 | address-store | variable,
address-store |
| ast2 | address-store | variable,
address-store |
| aubifs-crash | aubifs-base | predicate,
node-index × key-set × key-set × node-index × key-set × node-store × address-list × node-index × key-set × key-set × node-index × key-set × node-store × address-list |
| aubifs_core_check_commit# | aubifs-internal-asm | procedure,
node-index × key-set
: node-index × key-set × node-store × address-list × bool
: error |
| aubifs_core_commit# | aubifs-internal-asm | procedure,
node-index × key-set
: node-store × node-index × key-set × address-list
: bool × error |
| aubifs_core_format# | aubifs-internal-asm | procedure,
nat × nat × bool
:
: node-index × node-index × key-set × key-set × node-store ×
address-list × bool × error |
| aubifs_core_gc_copy# | aubifs-internal-asm | procedure,
: node-index × node-store × address-list |
| aubifs_core_gc_drop# | aubifs-internal-asm | procedure,
node-index × address-list : node-store |
| aubifs_core_index_contains# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: bool
: error |
| aubifs_core_index_entries# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: stringset
: error |
| aubifs_core_index_lookup# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: bool × node
: error |
| aubifs_core_index_newino# | aubifs-internal-asm | procedure,
node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: key |
| aubifs_core_index_remove# | aubifs-internal-asm | procedure,
key × node-index × key-set × key-set × node-store × address-list ×
bool
: node-index |
| aubifs_core_index_store# | aubifs-internal-asm | procedure,
key × address × node-index × key-set × key-set × node-store ×
address-list × bool
: node-index |
| aubifs_core_index_truncate# | aubifs-internal-asm | procedure,
key × nat × node-index × key-set × key-set × node-store × address-list ×
bool
: node-index |
| aubifs_core_journal_add1# | aubifs-internal-asm | procedure,
node × node-index × node-index × key-set × key-set
: address × node-store × address-list
: bool × error |
| aubifs_core_journal_add2# | aubifs-internal-asm | procedure,
node × node × node-index × node-index × key-set × key-set
: address × address × node-store × address-list
: bool × error |
| aubifs_core_journal_add3# | aubifs-internal-asm | procedure,
node × node × node × node-index × node-index × key-set × key-set
: address × address × address × node-store × address-list
: bool × error |
| aubifs_core_journal_add4# | aubifs-internal-asm | procedure,
node × node × node × node × node-index × node-index × key-set ×
key-set
: address × address × address × address × node-store × address-list
: bool × error |
| aubifs_core_journal_add5# | aubifs-internal-asm | procedure,
node × node × node × node × node × node-index × node-index × key-set ×
key-set
: address × address × address × address × address × node-store ×
address-list
: bool × error |
| aubifs_core_journal_gc# | aubifs-internal-asm | procedure,
node-index × key-set × key-set
: node-index × node-store × address-list
: bool |
| aubifs_core_journal_get# | aubifs-internal-asm | procedure,
address × node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: node
: error |
| aubifs_core_journal_sync# | aubifs-internal-asm | procedure,
node-index × node-index × key-set × key-set × node-store ×
address-list
:
: bool × error |
| aubifs_core_orphans_contains# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × key-set × node-store ×
address-list × bool
: bool |
| aubifs_core_orphans_insert# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × node-store × address-list ×
bool
: key-set |
| aubifs_core_orphans_remove# | aubifs-internal-asm | procedure,
key × node-index × node-index × key-set × node-store × address-list ×
bool
: key-set |
| aubifs_core_recover# | aubifs-internal-asm | procedure,
bool
: address-list × key-set × node-index × key-set × key-set ×
address-list × node-store
: node-index × bool × error |
| ax | address-list-set | variable,
address-list |
| ax0 | address-list-set | variable,
address-list |
| ax1 | address-list-set | variable,
address-list |
| ay | address-list-set | variable,
address-list |
| az | address-list-set | variable,
address-list |
| b | elem | variable,
elem |
| boolvar | node | variable,
bool |
| boolvar | inode | variable,
bool |
| boolvar | indexnode | variable,
bool |
| boolvar0 | node | variable,
bool |
| boolvar0 | inode | variable,
bool |
| boolvar0 | indexnode | variable,
bool |
| boolvar1 | groupnode | variable,
bool |
| boolvar2 | groupnode | variable,
bool |
| br | branch | variable,
branch |
| br0 | branch-array | variable,
branch |
| br1 | branch-array | variable,
branch |
| branch | branch | sort,
|
| branch-array | branch-array | sort,
|
| brar | branch-array | variable,
branch-array |
| brar0 | branch-array | variable,
branch-array |
| brar1 | branch-array | variable,
branch-array |
| brar2 | branch-array | variable,
branch-array |
| buf | buffer | variable,
buffer |
| buf0 | buffer | variable,
buffer |
| buf1 | buffer | variable,
buffer |
| buf2 | buffer | variable,
buffer |
| buffer | buffer | sort,
|
| butlastn | address-list-set | partial function,
nat × address-list → address-list |
| butlastn | list-last | partial function,
nat × list → list |
| butlastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| butlastn | group-store | partial function,
nat × group-node-list → group-node-list |
| butlastn | index-store | partial function,
nat × index-node-list → index-node-list |
| butlastn | key-list-set | partial function,
nat × key-list → key-list |
| butlastn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| butlastn | node-list | partial function,
nat × node-list → node-list |
| butlastn | string | partial function,
nat × string → string |
| c | elem | variable,
elem |
| char | char | variable,
char |
| char | char | sort,
|
| char0 | char | variable,
char |
| char1 | char | variable,
char |
| char2 | char | variable,
char |
| cmp | array-copy | partial predicate,
array × elem × nat × nat |
| cmp | array-copy | partial predicate,
array × nat × array × nat × nat |
| cmp | buffer | partial predicate,
buffer × data × nat × nat |
| cmp | buffer | partial predicate,
buffer × nat × buffer × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × branch × nat × nat |
| cmp | branch-array | partial predicate,
branch-array × nat × branch-array × nat × nat |
| copy | array-copy | partial function,
array × nat × array × nat × nat → array |
| copy | buffer | partial function,
buffer × nat × buffer × nat × nat → buffer |
| copy | branch-array | partial function,
branch-array × nat × branch-array × nat × nat → branch-array |
| crash | apersistence-base | function,
group-store × group-store × nat-set × nat-list → group-store |
| crash | apersistence-base | function,
index-store × index-store → index-store |
| crash-logblock | apersistence-base | function,
group-block × nat → group-block |
| d | data | variable,
data |
| d0 | data | variable,
data |
| d1 | data | variable,
data |
| d2 | data | variable,
data |
| data | data | sort,
|
| dataf | ablock-store | variable,
ablock → ablock |
| dataf | store-map | variable,
data → data |
| datakey | key | function,
nat × nat → key |
| datakeys | aubifs-base | function,
key-set × node-index → key-set |
| datakeys | aubifs-base | function,
key × nat × node-index → key-set |
| datakeys | aubifs-base | function,
key × node-index → key-set |
| datanode | node | function,
key × buffer → node |
| debug# | debug | procedure,
string : |
| dent | dentry | variable,
dentry |
| dentries | aubifs-base | function,
key × node-index → stringset |
| dentry | dentry | sort,
|
| dentrykey | key | function,
nat × string → key |
| dentrykeys | aubifs-base | function,
key × node-index → key-set |
| dentrynode | node | function,
key × nat → node |
| disj | address-list-set | predicate,
address-list × address-list |
| disj | list-dup | predicate,
list × list |
| disj | nat-list-set | predicate,
nat-list × nat-list |
| disj | group-store | predicate,
group-node-list × group-node-list |
| disj | index-store | predicate,
index-node-list × index-node-list |
| disj | key-list-set | predicate,
key-list × key-list |
| disj | laddress-list | predicate,
laddress-list × laddress-list |
| disj | node-list | predicate,
node-list × node-list |
| disj | string | predicate,
string × string |
| dom | node-store | function,
node-store → address-set |
| dom | node-index | function,
node-index → key-set |
| dom | store+set | function,
store → set |
| dom | group-store | function,
group-address-store → address-set |
| dom | group-store | function,
group-store → nat-set |
| dom | index-store | function,
index-address-store → address-set |
| dom | index-store | function,
index-store → nat-set |
| dom | nat-store | function,
store → nat-set |
| dom | address-store | function,
address-store → address-set |
| dropn | address-list-set | function,
nat × address-list → address-list |
| dropn | nat-list-set | function,
nat × nat-list → nat-list |
| dropn | group-store | function,
nat × group-node-list → group-node-list |
| dropn | index-store | function,
nat × index-node-list → index-node-list |
| dropn | key-list-set | function,
nat × key-list → key-list |
| dropn | laddress-list | function,
nat × laddress-list → laddress-list |
| dropn | list-prefixn | function,
nat × list → list |
| dropn | node-list | function,
nat × node-list → node-list |
| dups | address-list-set | predicate,
address-list |
| dups | list-dup | predicate,
list |
| dups | nat-list-set | predicate,
nat-list |
| dups | group-store | predicate,
group-node-list |
| dups | index-store | predicate,
index-node-list |
| dups | key-list-set | predicate,
key-list |
| dups | laddress-list | predicate,
laddress-list |
| dups | node-list | predicate,
node-list |
| dups | string | predicate,
string |
| elem | elem | sort,
|
| elemdataf | nat-store | variable,
nat × data → data |
| elemdataf | ablock-store | variable,
nat × ablock → ablock |
| elemdataf | store-map | variable,
elem × data → data |
| elemf | address-store | variable,
elem → elem |
| elems | apersistence-base | function,
nat-list → nat-set |
| empty | array-splice | constant,
elem |
| empty | buffer | constant,
data |
| emptyleb | eraseblock | constant,
buffer |
| emptypage | eraseblock | constant,
buffer |
| emptypeb | eraseblock | constant,
buffer |
| err | error | variable,
error |
| err0 | error | variable,
error |
| err1 | error | variable,
error |
| error | error | sort,
|
| fail# | error-class | procedure,
: : error |
| fail_or_success# | error-class | procedure,
: : error |
| fi | aubifs-base | variable,
node-index |
| fi0 | aubifs-base | variable,
node-index |
| fi1 | aubifs-base | variable,
node-index |
| fi2 | aubifs-base | variable,
node-index |
| file-node-cons | aubifs-inv | predicate,
node-store × node-index |
| fill | array-copy | partial function,
array × elem × nat × nat → array |
| fill | array-copy | function,
array × elem → array |
| fill | buffer | partial function,
buffer × data × nat × nat → buffer |
| fill | buffer | function,
buffer × data → buffer |
| fill | branch-array | partial function,
branch-array × branch × nat × nat → branch-array |
| fill | branch-array | function,
branch-array × branch → branch-array |
| fillfirst | address-list-set | function,
nat × address × address-list → address-list |
| fillfirst | list-last | function,
nat × elem × list → list |
| fillfirst | nat-list-set | function,
nat × nat × nat-list → nat-list |
| fillfirst | group-store | function,
nat × group-node × group-node-list → group-node-list |
| fillfirst | index-store | function,
nat × index-node × index-node-list → index-node-list |
| fillfirst | key-list-set | function,
nat × key × key-list → key-list |
| fillfirst | laddress-list | function,
nat × laddress × laddress-list → laddress-list |
| fillfirst | node-list | function,
nat × node × node-list → node-list |
| fillfirst | string | function,
nat × char × string → string |
| firstn | address-list-set | partial function,
nat × address-list → address-list |
| firstn | list-del | partial function,
nat × list → list |
| firstn | nat-list-set | partial function,
nat × nat-list → nat-list |
| firstn | group-store | partial function,
nat × group-node-list → group-node-list |
| firstn | index-store | partial function,
nat × index-node-list → index-node-list |
| firstn | key-list-set | partial function,
nat × key-list → key-list |
| firstn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| firstn | node-list | partial function,
nat × node-list → node-list |
| firstn | string | partial function,
nat × string → string |
| fo | aubifs-base | variable,
key-set |
| fo0 | aubifs-base | variable,
key-set |
| fo1 | aubifs-base | variable,
key-set |
| fo2 | aubifs-base | variable,
key-set |
| frome | address-list-set | function,
address-list × address → address-list |
| frome | list-del | function,
list × elem → list |
| frome | nat-list-set | function,
nat-list × nat → nat-list |
| frome | group-store | function,
group-node-list × group-node → group-node-list |
| frome | index-store | function,
index-node-list × index-node → index-node-list |
| frome | key-list-set | function,
key-list × key → key-list |
| frome | laddress-list | function,
laddress-list × laddress → laddress-list |
| frome | node-list | function,
node-list × node → node-list |
| frome | string | function,
string × char → string |
| fs | node-store | variable,
node-store |
| fs0 | node-store | variable,
node-store |
| fs1 | node-store | variable,
node-store |
| fs2 | node-store | variable,
node-store |
| gast | group-store | variable,
group-address-store |
| gast0 | group-store | variable,
group-address-store |
| gast1 | group-store | variable,
group-address-store |
| gast2 | group-store | variable,
group-address-store |
| gblock | group-store | variable,
group-block |
| gblock0 | group-store | variable,
group-block |
| gblock1 | group-store | variable,
group-block |
| gblock2 | group-store | variable,
group-block |
| gdataf | group-store | variable,
group-block → group-block |
| gelemdataf | group-store | variable,
nat × group-block → group-block |
| gelemf | group-store | variable,
group-node → group-node |
| ginval | apersistence-base | variable,
nat-set |
| gjournal_check_commit# | gjournal-asm | procedure,
nat × nat-set × node-index
: node-index × nat-set × group-store × group-store × nat-list × nat ×
nat-set × bool
: error |
| gjournal_commit# | gjournal-asm | procedure,
nat × nat-set × node-index
: node-index × nat-set × group-store × group-store × nat-list × nat ×
nat-set × bool
: error |
| gjournal_format# | gjournal-asm | procedure,
nat × nat × bool
: nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool × nat × nat-set × bool × error |
| gjournal_gc_copy# | gjournal-asm | procedure,
bool × node-index × group-store × nat × nat-set
: node-list × bool × nat × nat × node-index × nat-set × group-store ×
nat-list × bool
: error |
| gjournal_gc_referenced_nodes# | gjournal-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-list × group-node-list
: node-list × error |
| gjournal_gc_update_index# | gjournal-asm | procedure,
bool × node-index × nat-set × group-store × nat-list × nat × nat-set ×
bool
: address-list × node-list × nat × node-index × group-store |
| gjournal_index_contains# | gjournal-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool
: error |
| gjournal_index_entries# | gjournal-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: stringset
: error |
| gjournal_index_lookup# | gjournal-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool × node
: error |
| gjournal_index_newino# | gjournal-asm | procedure,
: key × nat |
| gjournal_index_remove# | gjournal-asm | procedure,
key × node-index × nat-set × group-store × nat-list × nat × nat-set ×
bool
: node-index × group-store |
| gjournal_index_store# | gjournal-asm | procedure,
key × address × node-index × nat-set × group-store × nat-list × nat ×
nat-set × bool
: nat × node-index × group-store |
| gjournal_index_truncate# | gjournal-asm | procedure,
key × nat × bool × node-index × nat-set × group-store × nat-list × nat ×
nat-set × bool
: node-index × group-store |
| gjournal_journal_add1# | gjournal-asm | procedure,
node × bool × node-index × node-index × group-store × nat × nat-set
: address × bool × nat × nat-set × group-store × nat-list × bool
: error |
| gjournal_journal_add2# | gjournal-asm | procedure,
node × node × bool × node-index × node-index × group-store × nat ×
nat-set
: address × address × bool × nat × nat-set × group-store × nat-list ×
bool
: error |
| gjournal_journal_add3# | gjournal-asm | procedure,
node × node × node × bool × node-index × node-index × group-store ×
nat × nat-set
: address × address × address × bool × nat × nat-set × group-store ×
nat-list × bool
: error |
| gjournal_journal_add4# | gjournal-asm | procedure,
node × node × node × node × bool × node-index × node-index ×
group-store × nat × nat-set
: address × address × address × address × bool × nat × nat-set ×
group-store × nat-list × bool
: error |
| gjournal_journal_add5# | gjournal-asm | procedure,
node × node × node × node × node × bool × node-index × node-index ×
group-store × nat × nat-set
: address × address × address × address × address × bool × nat ×
nat-set × group-store × nat-list × bool
: error |
| gjournal_journal_addn# | gjournal-asm | procedure,
node-list × bool × node-index × node-index × group-store × nat ×
nat-set
: address-list × bool × nat × nat-set × group-store × nat-list × bool
: error |
| gjournal_journal_allocate# | gjournal-asm | procedure,
nat × node-index × node-index × group-store × nat × nat-set
: bool × nat-set × group-store × nat-list × bool
: error |
| gjournal_journal_gc# | gjournal-asm | procedure,
bool × node-index × group-store × nat × nat-set
: bool × nat × nat × node-index × nat-set × group-store × nat-list ×
bool |
| gjournal_journal_get# | gjournal-asm | procedure,
address × node-index × node-index × nat-set × group-store ×
group-store × nat-list × nat × nat-set × bool
: node
: error |
| gjournal_journal_sync# | gjournal-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set
: bool
: error |
| gjournal_journal_transaction# | gjournal-asm | procedure,
node-list × nat : : group-node-list × nat |
| gjournal_orphans_contains# | gjournal-asm | procedure,
key × nat-set : bool |
| gjournal_orphans_insert# | gjournal-asm | procedure,
key : nat × nat-set |
| gjournal_orphans_remove# | gjournal-asm | procedure,
key : nat-set |
| gjournal_recover# | gjournal-asm | procedure,
bool
: address-list × key-set × nat × nat-set × node-index × node-index ×
nat-set × group-store × group-store × nat-list × nat × nat-set ×
bool
: bool × nat × bool × error |
| gjournal_remove_addresses# | gjournal-asm | procedure,
bool × node-index × node-index × nat-set × group-store × nat-list ×
nat × nat-set × bool
: address-set × group-store |
| gjournal_remove_nonend_blocks# | gjournal-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-list
: error |
| gjournal_restore_log# | gjournal-asm | procedure,
nat-list × node-index × node-index × nat-set × group-store ×
group-store × nat-list × nat × nat-set × bool
: address-list
: error |
| gjournal_split_nodes# | gjournal-asm | procedure,
nat : node-list × node-list |
| gnd | groupnode | variable,
group-node |
| gnd0 | group-store | variable,
group-node |
| gnd1 | group-store | variable,
group-node |
| gnd2 | group-store | variable,
group-node |
| gndx | group-store | variable,
group-node-list |
| gndx0 | group-store | variable,
group-node-list |
| gndx1 | group-store | variable,
group-node-list |
| gndx2 | group-store | variable,
group-node-list |
| gndx3 | group-store | variable,
group-node-list |
| group-address-store | group-store | sort,
|
| group-block | group-store | sort,
|
| group-node | groupnode | sort,
|
| group-node-list | group-store | sort,
|
| group-store | group-store | sort,
|
| groupblock | group-store | function,
group-node-list × laddress-list × nat → group-block |
| gstore | group-store | variable,
group-store |
| gstore0 | group-store | variable,
group-store |
| gstore1 | group-store | variable,
group-store |
| gstore2 | group-store | variable,
group-store |
| iast | index-store | variable,
index-address-store |
| iast0 | index-store | variable,
index-address-store |
| iast1 | index-store | variable,
index-address-store |
| iast2 | index-store | variable,
index-address-store |
| iblock | index-store | variable,
index-block |
| iblock0 | index-store | variable,
index-block |
| iblock1 | index-store | variable,
index-block |
| iblock2 | index-store | variable,
index-block |
| idataf | index-store | variable,
index-block → index-block |
| idrange | array-copy | partial predicate,
array × nat × nat |
| idrange | buffer | partial predicate,
buffer × nat × nat |
| idrange | branch-array | partial predicate,
branch-array × nat × nat |
| id○ | array-copy | predicate,
array × array × nat |
| id○ | buffer | predicate,
buffer × buffer × nat |
| id○ | branch-array | predicate,
branch-array × branch-array × nat |
| ielemdataf | index-store | variable,
nat × index-block → index-block |
| ielemf | index-store | variable,
index-node → index-node |
| ind | indexnode | variable,
index-node |
| ind0 | index-store | variable,
index-node |
| ind1 | index-store | variable,
index-node |
| ind2 | index-store | variable,
index-node |
| index | persistence-state | function,
nat → persistence-state |
| index-address-store | index-store | sort,
|
| index-block | index-store | sort,
|
| index-node | indexnode | sort,
|
| index-node-list | index-store | sort,
|
| index-store | index-store | sort,
|
| index_add_gnds# | index-asm | procedure,
group-node-list × node-index × node-index × nat-set × group-store ×
nat-list × nat × nat-set
: address-list × group-store
: bool × error |
| index_allocate_gnd# | index-asm | procedure,
node-index × node-index × group-store × nat × nat-set × bool
: nat-set × group-store × nat-list
: error |
| index_commit# | index-asm | procedure,
nat × node-index × bool
: nat-set × nat-set × group-store × node-index × group-store ×
nat-list × nat × nat-set
: error |
| index_deallocate_gnd# | index-asm | procedure,
nat × node-index × node-index × group-store × nat-list × nat × nat-set ×
bool
: nat-set × group-store
: error |
| index_format# | index-asm | procedure,
nat × nat × nat
:
: node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool × error |
| index_get_block_free_size# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_get_gblock_refsize# | index-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_get_gc_block# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: nat
: error |
| index_get_leb_size | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: nat |
| index_index_contains# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool
: error |
| index_index_entries# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: stringset
: error |
| index_index_lookup# | index-asm | procedure,
key × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: bool × address
: error |
| index_index_remove# | index-asm | procedure,
key × node-index × nat-set × group-store × group-store × nat-list ×
nat × nat-set × bool
: address × bool × node-index |
| index_index_store# | index-asm | procedure,
key × address × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address × bool × node-index |
| index_index_truncate# | index-asm | procedure,
key × nat × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-set × node-index |
| index_is_log_empty# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: bool |
| index_read_gblock_nodes# | index-asm | procedure,
nat × node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
: address-list × group-node-list
: error |
| index_read_gnd# | index-asm | procedure,
address × node-index × node-index × nat-set × group-store ×
group-store × nat-list × nat × nat-set × bool
: group-node
: error |
| index_recover# | index-asm | procedure,
: nat × nat-list × nat-set × node-index × nat-list × nat × nat-set ×
nat-set × group-store × group-store
: node-index × bool × error |
| index_requires_commit# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set × bool
:
: bool |
| index_set_gblock_refsize# | index-asm | procedure,
nat × nat × node-index × node-index × nat-set × group-store × nat-list ×
nat × nat-set × bool
: group-store |
| index_sync# | index-asm | procedure,
node-index × node-index × nat-set × group-store × group-store ×
nat-list × nat × nat-set
:
: bool × error |
| indexblock | index-store | function,
index-node-list × laddress-list × nat → index-block |
| indexnode | indexnode | function,
branch-array × bool × nat → index-node |
| indx | index-store | variable,
index-node-list |
| indx0 | index-store | variable,
index-node-list |
| indx1 | index-store | variable,
index-node-list |
| indx2 | index-store | variable,
index-node-list |
| indx3 | index-store | variable,
index-node-list |
| ino | aubifs-base | variable,
nat |
| ino0 | aubifs-base | variable,
nat |
| ino1 | aubifs-base | variable,
nat |
| ino2 | aubifs-base | variable,
nat |
| inode | inode | variable,
inode |
| inode | inode | sort,
|
| inodekey | key | function,
nat → key |
| inodenode | node | function,
key × metadata × bool × nat × nat × nat → node |
| inv | group-store | predicate,
group-store |
| inv | group-store | predicate,
group-block |
| inv | index-store | predicate,
index-store |
| inv | index-store | predicate,
index-block |
| inv | ablock-store-inv | predicate,
store |
| inv | ablock-store-inv | predicate,
ablock |
| inv | apersistence-base | predicate,
nat-list × group-store × group-store × nat-set × index-store × index-store |
| inv-flashsize | group-store | predicate,
group-node-list × laddress-list |
| inv-flashsize | index-store | predicate,
index-node-list × laddress-list |
| inv-flashsize | ablock-store-inv | predicate,
list × laddress-list |
| inv-index | apersistence-base | predicate,
index-store × index-store |
| inv-journal | apersistence-base | predicate,
nat-list × group-store × group-store × nat-set |
| inv-state | apersistence-base | predicate,
persistence-state × nat-list × group-store × index-store × bool |
| is-aligned | align | predicate,
nat × nat |
| isempty | eraseblock | predicate,
buffer × nat × nat |
| isempty | eraseblock | predicate,
buffer |
| istore | index-store | variable,
index-store |
| istore0 | index-store | variable,
index-store |
| istore1 | index-store | variable,
index-store |
| istore2 | index-store | variable,
index-store |
| jmaxino | gjournal-asm | variable,
nat |
| journal | persistence-state | function,
nat → persistence-state |
| jro | gjournal-asm | variable,
nat-set |
| jvalid | gjournal-asm | variable,
bool |
| key | key | variable,
key |
| key | key | sort,
|
| key-cons | gjournal-base | predicate,
node-list |
| key-cons | gjournal-base | predicate,
key-list × address-list × group-store × nat-set |
| key-cons | aubifs-inv | predicate,
key × node |
| key-list | key-list-set | sort,
|
| key-set | node-index | sort,
|
| key-set | key-list-set | sort,
|
| key0 | node-index | variable,
key |
| key0 | node | variable,
key |
| key0 | key-list-set | variable,
key |
| key0 | branch | variable,
key |
| key1 | node-index | variable,
key |
| key1 | key-list-set | variable,
key |
| key2 | key-list-set | variable,
key |
| keys | aubifs-base | function,
node-store × address-list → key-list |
| ks | node-index | variable,
key-set |
| ks | key-list-set | variable,
key-set |
| ks0 | node-index | variable,
key-set |
| ks0 | key-list-set | variable,
key-set |
| ks1 | node-index | variable,
key-set |
| ks1 | key-list-set | variable,
key-set |
| ks2 | node-index | variable,
key-set |
| ks2 | key-list-set | variable,
key-set |
| kx | key-list-set | variable,
key-list |
| kx0 | key-list-set | variable,
key-list |
| kx1 | key-list-set | variable,
key-list |
| ky | key-list-set | variable,
key-list |
| kz | key-list-set | variable,
key-list |
| laddress | laddress | sort,
|
| laddress-list | laddress-list | sort,
|
| ladr | laddress | variable,
laddress |
| ladr0 | laddress-list | variable,
laddress |
| ladr1 | laddress-list | variable,
laddress |
| ladr2 | laddress-list | variable,
laddress |
| lastn | address-list-set | partial function,
nat × address-list → address-list |
| lastn | list-del | partial function,
nat × list → list |
| lastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| lastn | group-store | partial function,
nat × group-node-list → group-node-list |
| lastn | index-store | partial function,
nat × index-node-list → index-node-list |
| lastn | key-list-set | partial function,
nat × key-list → key-list |
| lastn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| lastn | node-list | partial function,
nat × node-list → node-list |
| lastn | string | partial function,
nat × string → string |
| lax | laddress-list | variable,
laddress-list |
| lax0 | laddress-list | variable,
laddress-list |
| lax1 | laddress-list | variable,
laddress-list |
| lax2 | laddress-list | variable,
laddress-list |
| lax3 | laddress-list | variable,
laddress-list |
| ld | aubifs-base | variable,
key-set |
| ld0 | aubifs-base | variable,
key-set |
| ld1 | aubifs-base | variable,
key-set |
| ld2 | aubifs-base | variable,
key-set |
| links | aubifs-base | function,
nat × node-store × node-index → key-set |
| list | list-data | sort,
|
| lnum | gjournal-abs | variable,
nat |
| log | aubifs-base | variable,
address-list |
| log-cons | aubifs-inv | predicate,
address-list × node-store |
| log0 | aubifs-base | variable,
address-list |
| log1 | aubifs-base | variable,
address-list |
| log2 | aubifs-base | variable,
address-list |
| m | nat-basic | variable,
nat |
| m0 | array-copy | variable,
nat |
| m0 | address-data | variable,
nat |
| m0 | inode | variable,
nat |
| m0 | dentry | variable,
nat |
| m0 | key | variable,
nat |
| m0 | laddress | variable,
nat |
| m0 | persistence-state | variable,
nat |
| m1 | address-data | variable,
nat |
| m1 | inode | variable,
nat |
| m1 | key | variable,
nat |
| m1 | laddress | variable,
nat |
| m2 | address-data | variable,
nat |
| m2 | inode | variable,
nat |
| m2 | key | variable,
nat |
| m2 | laddress | variable,
nat |
| m3 | node | variable,
nat |
| m3 | address-data | variable,
nat |
| m3 | inode | variable,
nat |
| m4 | node | variable,
nat |
| m4 | address-data | variable,
nat |
| m4 | inode | variable,
nat |
| m5 | inode | variable,
nat |
| m6 | inode | variable,
nat |
| max | min-max | function,
nat × nat → nat |
| maxino | apersistence-base | variable,
nat |
| md | metadata | variable,
metadata |
| md0 | node | variable,
metadata |
| md0 | inode | variable,
metadata |
| metadata | metadata | sort,
|
| min | min-max | function,
nat × nat → nat |
| mkarray | array | function,
nat → array |
| mkblock | ablock | function,
list × laddress-list × nat → ablock |
| mkbranch | branch | function,
key × address → branch |
| mkbrarray | branch-array | function,
nat → branch-array |
| mkbuf | buffer | function,
nat → buffer |
| mkdentry | dentry | function,
string × nat → dentry |
| mkemparray | array-splice | function,
nat → array |
| mkempbuf | buffer | function,
nat → buffer |
| mkentry | branch | function,
key × address → branch |
| mkgnode | groupnode | function,
node × nat × bool × bool → group-node |
| mkinode | inode | function,
nat × metadata × bool × nat × nat × nat → inode |
| mklist | address-list-set | function,
address × nat → address-list |
| mklist | list-last | function,
elem × nat → list |
| mklist | nat-list-set | function,
nat × nat → nat-list |
| mklist | group-store | function,
group-node × nat → group-node-list |
| mklist | index-store | function,
index-node × nat → index-node-list |
| mklist | key-list-set | function,
key × nat → key-list |
| mklist | laddress-list | function,
laddress × nat → laddress-list |
| mklist | node-list | function,
node × nat → node-list |
| mklist | string | function,
char × nat → string |
| mkzarray | array-splice | function,
nat → array |
| mkzbuf | buffer | function,
nat → buffer |
| n | nat-basic | variable,
nat |
| n0 | nat-basic | variable,
nat |
| n1 | nat-basic | variable,
nat |
| n2 | nat-list-set | variable,
nat |
| n2 | nat-store | variable,
nat |
| n2 | nat-set | variable,
nat |
| n3 | nat-list-set | variable,
nat |
| n3 | nat-store | variable,
nat |
| n3 | nat-set | variable,
nat |
| n4 | nat-list-set | variable,
nat |
| n4 | nat-store | variable,
nat |
| n4 | nat-set | variable,
nat |
| n5 | nat-list-set | variable,
nat |
| nat | nat-basic | sort,
|
| nat-list | nat-list-set | sort,
|
| nat-set | nat-list-set | sort,
|
| nat-set | nat-store | sort,
|
| nat-set | nat-set | sort,
|
| nd | node | variable,
node |
| nd0 | node | variable,
node |
| nd1 | node | variable,
node |
| nd2 | node | variable,
node |
| nd3 | node | variable,
node |
| ndx | node-list | variable,
node-list |
| ndx0 | node-list | variable,
node-list |
| ndx1 | node-list | variable,
node-list |
| ndy | node-list | variable,
node-list |
| ndz | node-list | variable,
node-list |
| negdentry | dentry | function,
string → dentry |
| new | aubifs-base | predicate,
address-list × node-store |
| node | node | sort,
|
| node-closed | aubifs-inv | predicate,
node × node-index × node-store × key-set |
| node-cons | aubifs-inv | predicate,
key × node |
| node-index | node-index | sort,
|
| node-list | node-list | sort,
|
| node-store | node-store | sort,
|
| nodes | group-store | function,
group-store → group-address-store |
| nodes | index-store | function,
index-store → index-address-store |
| nodes | gjournal-abs | function,
nat × group-block → node-store |
| nodes | gjournal-abs | function,
group-store × nat-set → node-store |
| nodes | ablock-nodes | function,
store → address-store |
| nodes-cons | gjournal-base | predicate,
address-list × node-list × group-store × nat-set |
| ns | nat-list-set | variable,
nat-set |
| ns | nat-store | variable,
nat-set |
| ns | nat-set | variable,
nat-set |
| ns0 | nat-list-set | variable,
nat-set |
| ns0 | nat-store | variable,
nat-set |
| ns0 | nat-set | variable,
nat-set |
| ns1 | nat-list-set | variable,
nat-set |
| ns1 | nat-store | variable,
nat-set |
| ns1 | nat-set | variable,
nat-set |
| ns2 | nat-list-set | variable,
nat-set |
| ns2 | nat-store | variable,
nat-set |
| ns2 | nat-set | variable,
nat-set |
| nx | nat-list-set | variable,
nat-list |
| nx0 | nat-list-set | variable,
nat-list |
| nx1 | nat-list-set | variable,
nat-list |
| ny | nat-list-set | variable,
nat-list |
| nz | nat-list-set | variable,
nat-list |
| orphans | aubifs-inv | function,
node-store × node-index → key-set |
| os | aubifs-internal-asm | variable,
key-set |
| p_os | gjournal-asm | variable,
nat-set |
| persistence-state | persistence-state | sort,
|
| pmaxino | gjournal-asm | variable,
nat |
| pos | address-list-set | function,
address × address-list → nat |
| pos | list-del | function,
elem × list → nat |
| pos | nat-list-set | function,
nat × nat-list → nat |
| pos | group-store | function,
group-node × group-node-list → nat |
| pos | index-store | function,
index-node × index-node-list → nat |
| pos | key-list-set | function,
key × key-list → nat |
| pos | laddress-list | function,
laddress × laddress-list → nat |
| pos | node-list | function,
node × node-list → nat |
| pos | string | function,
char × string → nat |
| prefixn | address-list-set | function,
nat × address-list → address-list |
| prefixn | nat-list-set | function,
nat × nat-list → nat-list |
| prefixn | group-store | function,
nat × group-node-list → group-node-list |
| prefixn | index-store | function,
nat × index-node-list → index-node-list |
| prefixn | key-list-set | function,
nat × key-list → key-list |
| prefixn | laddress-list | function,
nat × laddress-list → laddress-list |
| prefixn | list-prefixn | function,
nat × list → list |
| prefixn | node-list | function,
nat × node-list → node-list |
| pstate | persistence-state | variable,
persistence-state |
| range | aubifs-base | function,
node-index → address-set |
| range= | array-splice | predicate,
array × nat × array × nat × nat |
| range= | buffer | predicate,
buffer × nat × buffer × nat × nat |
| readonly | persistence-state | constant,
persistence-state |
| referenced-adrs | gjournal-base | function,
address-list × node-index → address-list |
| refsize-cons | group-store | predicate,
group-store × address-set |
| refsize-cons | index-store | predicate,
index-store × address-set |
| refsize-cons | ablock-store-refsize-cons | predicate,
store × address-set |
| refsize0-addresses | gjournal-abs | function,
group-store → address-set |
| remove-nonend-inv | gjournal-abs | predicate,
address-list × address-list × address-list × group-node-list × group-node-list × bool |
| remove-refsize0 | group-store | function,
group-store → group-store |
| remove-refsize0 | index-store | function,
index-store → index-store |
| remove-refsize0 | ablock-store-inv | function,
store → store |
| resize | array-splice | function,
array × nat → array |
| resize | buffer | function,
buffer × nat → buffer |
| restn | address-list-set | partial function,
nat × address-list → address-list |
| restn | list-del | partial function,
nat × list → list |
| restn | nat-list-set | partial function,
nat × nat-list → nat-list |
| restn | group-store | partial function,
nat × group-node-list → group-node-list |
| restn | index-store | partial function,
nat × index-node-list → index-node-list |
| restn | key-list-set | partial function,
nat × key-list → key-list |
| restn | laddress-list | partial function,
nat × laddress-list → laddress-list |
| restn | node-list | partial function,
nat × node-list → node-list |
| restn | string | partial function,
nat × string → string |
| restore-log-inv | gjournal-abs | predicate,
nat-list × nat-list × group-store × nat-set × address-list × error |
| rev | address-list-set | function,
address-list → address-list |
| rev | array-copy | partial function,
array × nat → array |
| rev | array-copy | function,
array → array |
| rev | list-last | function,
list → list |
| rev | buffer | partial function,
buffer × nat → buffer |
| rev | buffer | function,
buffer → buffer |
| rev | nat-list-set | function,
nat-list → nat-list |
| rev | group-store | function,
group-node-list → group-node-list |
| rev | index-store | function,
index-node-list → index-node-list |
| rev | key-list-set | function,
key-list → key-list |
| rev | laddress-list | function,
laddress-list → laddress-list |
| rev | branch-array | partial function,
branch-array × nat → branch-array |
| rev | branch-array | function,
branch-array → branch-array |
| rev | node-list | function,
node-list → node-list |
| rev | string | function,
string → string |
| ri | node-index | variable,
node-index |
| ri-closed | aubifs-inv | predicate,
node-index × node-store × key-set |
| ri-cons | aubifs-inv | predicate,
node-index × node-store |
| ri-inj | aubifs-inv | predicate,
node-index |
| ri0 | node-index | variable,
node-index |
| ri1 | node-index | variable,
node-index |
| ri2 | node-index | variable,
node-index |
| rmdup | address-list-set | function,
address-list → address-list |
| rmdup | list-dup | function,
list → list |
| rmdup | nat-list-set | function,
nat-list → nat-list |
| rmdup | group-store | function,
group-node-list → group-node-list |
| rmdup | index-store | function,
index-node-list → index-node-list |
| rmdup | key-list-set | function,
key-list → key-list |
| rmdup | laddress-list | function,
laddress-list → laddress-list |
| rmdup | node-list | function,
node-list → node-list |
| rmdup | string | function,
string → string |
| ro | aubifs-base | variable,
key-set |
| ro0 | aubifs-base | variable,
key-set |
| ro1 | aubifs-base | variable,
key-set |
| ro2 | aubifs-base | variable,
key-set |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| set | set-basic | sort,
|
| slice | address-list-set | function,
nat × nat × address-list → address-list |
| slice | nat-list-set | function,
nat × nat × nat-list → nat-list |
| slice | group-store | function,
nat × nat × group-node-list → group-node-list |
| slice | index-store | function,
nat × nat × index-node-list → index-node-list |
| slice | key-list-set | function,
nat × nat × key-list → key-list |
| slice | laddress-list | function,
nat × nat × laddress-list → laddress-list |
| slice | list-prefixn | function,
nat × nat × list → list |
| slice | node-list | function,
nat × nat × node-list → node-list |
| splice | array-splice | function,
array × nat × array × nat × nat → array |
| splice | buffer | function,
buffer × nat × buffer × nat × nat → buffer |
| st | store | variable,
store |
| st0 | store | variable,
store |
| st1 | store | variable,
store |
| st2 | store | variable,
store |
| store | store | sort,
|
| str | string | variable,
string |
| str0 | string | variable,
string |
| str1 | string | variable,
string |
| str2 | string | variable,
string |
| str3 | string | variable,
string |
| string | string | sort,
|
| strings | stringset | variable,
stringset |
| strings0 | stringset | variable,
stringset |
| strings1 | stringset | variable,
stringset |
| strings2 | stringset | variable,
stringset |
| stringset | stringset | sort,
|
| subarray | array-copy | partial function,
array × nat × nat → array |
| subarray | buffer | partial function,
buffer × nat × nat → buffer |
| subarray | branch-array | partial function,
branch-array × nat × nat → branch-array |
| sublist | address-list-set | partial function,
nat × nat × address-list → address-list |
| sublist | list-del | partial function,
nat × nat × list → list |
| sublist | nat-list-set | partial function,
nat × nat × nat-list → nat-list |
| sublist | group-store | partial function,
nat × nat × group-node-list → group-node-list |
| sublist | index-store | partial function,
nat × nat × index-node-list → index-node-list |
| sublist | key-list-set | partial function,
nat × nat × key-list → key-list |
| sublist | laddress-list | partial function,
nat × nat × laddress-list → laddress-list |
| sublist | node-list | partial function,
nat × nat × node-list → node-list |
| sublist | string | partial function,
nat × nat × string → string |
| syn | apersistence-base | variable,
bool |
| transaction | gjournal-base | predicate,
node-list × group-node-list |
| transaction-prefix | gjournal-base | predicate,
node-list × group-node-list |
| truncnode | node | function,
key × nat → node |
| ubifs-cons | aubifs-inv | predicate,
node-store × node-index × key-set × node-index × key-set × address-list |
| unbuffered | persistence-state | constant,
persistence-state |
| valid-adrs | ablock-store-refsize-cons | predicate,
address-set |
| valid-dentry | aubifs-base | predicate,
nat × dentry × node-store × node-index × key-set |
| valid-dentry | aubifs-base | predicate,
dentry × node-store × node-index × key-set |
| valid-dir-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-file-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-group-nodes | gjournal-abs | function,
group-node-list → nat |
| valid-ino | aubifs-base | predicate,
nat × node-store × node-index |
| valid-journal-head | gjournal-base | predicate,
nat-list × group-store × nat-set |
| valid-negdentry | aubifs-base | predicate,
nat × dentry × node-store × node-index × key-set |
| valid-parent-ino | aubifs-base | predicate,
nat × node-store × node-index × key-set |
| validhead | gjournal-abs | variable,
bool |
| x | list-data | variable,
list |
| x0 | list-data | variable,
list |
| x1 | list-data | variable,
list |
| y | list-data | variable,
list |
| z | list-data | variable,
list |
| zero | array-splice | constant,
elem |
| zero | buffer | constant,
data |
| zeropage | page | constant,
buffer |
| | | node-store | function,
node-store × address-set → node-store |
| | | node-index | function,
node-index × key-set → node-index |
| | | store+set | function,
store × set → store |
| | | group-store | function,
group-address-store × address-set → group-address-store |
| | | group-store | function,
group-store × nat-set → group-store |
| | | index-store | function,
index-address-store × address-set → index-address-store |
| | | index-store | function,
index-store × nat-set → index-store |
| | | nat-store | function,
store × nat-set → store |
| | | ablock-store-refsize-cons | function,
address-set × nat → address-set |
| | | address-store | function,
address-store × address-set → address-store |
| } | address-list-set | function,
address → address-set |
| } | node-store | function,
address → address-set |
| } | node-index | function,
key → key-set |
| } | set-union | function,
elem → set |
| } | nat-list-set | function,
nat → nat-set |
| } | stringset | function,
string → stringset |
| } | nat-store | function,
nat → nat-set |
| } | nat-set | function,
nat → nat-set |
| } | key-list-set | function,
key → key-set |
| } | address-store | function,
address → address-set |
| φ | gjournal-base | variable,
group-node-list → bool |
| ↓ | gjournal-abs | function,
group-store → group-store |
| ↓ | gjournal-abs | function,
group-block → group-block |
| ∅ | address-list-set | constant,
address-set |
| ∅ | node-store | constant,
address-set |
| ∅ | node-store | constant,
node-store |
| ∅ | node-index | constant,
key-set |
| ∅ | node-index | constant,
node-index |
| ∅ | set-basic | constant,
set |
| ∅ | store | constant,
store |
| ∅ | nat-list-set | constant,
nat-set |
| ∅ | group-store | constant,
group-address-store |
| ∅ | group-store | constant,
group-store |
| ∅ | index-store | constant,
index-address-store |
| ∅ | index-store | constant,
index-store |
| ∅ | stringset | constant,
stringset |
| ∅ | nat-store | constant,
nat-set |
| ∅ | nat-set | constant,
nat-set |
| ∅ | key-list-set | constant,
key-set |
| ∅ | address-store | constant,
address-set |
| ∅ | address-store | constant,
address-store |
| ∈ | address-list-set | predicate,
address × address-set |
| ∈ | address-list-set | predicate,
address × address-list |
| ∈ | node-store | predicate,
node × node-store |
| ∈ | node-store | predicate,
address × address-set |
| ∈ | node-store | predicate,
address × node-store |
| ∈ | node-index | predicate,
address × node-index |
| ∈ | node-index | predicate,
key × key-set |
| ∈ | node-index | predicate,
key × node-index |
| ∈ | store+set | predicate,
data × store |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | store | predicate,
elem × store |
| ∈ | array-copy | predicate,
elem × array |
| ∈ | list | predicate,
elem × list |
| ∈ | buffer | predicate,
data × buffer |
| ∈ | nat-list-set | predicate,
nat × nat-set |
| ∈ | nat-list-set | predicate,
nat × nat-list |
| ∈ | group-store | predicate,
group-node × group-address-store |
| ∈ | group-store | predicate,
address × group-address-store |
| ∈ | group-store | predicate,
address × group-store |
| ∈ | group-store | predicate,
group-block × group-store |
| ∈ | group-store | predicate,
nat × group-store |
| ∈ | group-store | predicate,
group-node × group-node-list |
| ∈ | index-store | predicate,
index-node × index-address-store |
| ∈ | index-store | predicate,
address × index-address-store |
| ∈ | index-store | predicate,
address × index-store |
| ∈ | index-store | predicate,
index-block × index-store |
| ∈ | index-store | predicate,
nat × index-store |
| ∈ | index-store | predicate,
index-node × index-node-list |
| ∈ | stringset | predicate,
string × stringset |
| ∈ | nat-store | predicate,
nat × nat-set |
| ∈ | nat-store | predicate,
nat × store |
| ∈ | nat-set | predicate,
nat × nat-set |
| ∈ | ablock-store | predicate,
ablock × store |
| ∈ | ablock-store-inv | predicate,
address × store |
| ∈ | key-list-set | predicate,
key × key-set |
| ∈ | key-list-set | predicate,
key × key-list |
| ∈ | laddress-list | predicate,
laddress × laddress-list |
| ∈ | branch-array | predicate,
branch × branch-array |
| ∈ | address-store | predicate,
elem × address-store |
| ∈ | address-store | predicate,
address × address-set |
| ∈ | address-store | predicate,
address × address-store |
| ∈ | node-list | predicate,
node × node-list |
| ∈ | string | predicate,
char × string |
| ∩ | address-list-set | function,
address-set × address-set → address-set |
| ∩ | node-store | function,
address-set × address-set → address-set |
| ∩ | node-index | function,
key-set × key-set → key-set |
| ∩ | set-union | function,
set × set → set |
| ∩ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∩ | stringset | function,
stringset × stringset → stringset |
| ∩ | nat-store | function,
nat-set × nat-set → nat-set |
| ∩ | nat-set | function,
nat-set × nat-set → nat-set |
| ∩ | key-list-set | function,
key-set × key-set → key-set |
| ∩ | address-store | function,
address-set × address-set → address-set |
| ∪ | address-list-set | function,
address-set × address-set → address-set |
| ∪ | node-store | function,
address-set × address-set → address-set |
| ∪ | node-index | function,
key-set × key-set → key-set |
| ∪ | set-union | function,
set × set → set |
| ∪ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∪ | stringset | function,
stringset × stringset → stringset |
| ∪ | nat-store | function,
nat-set × nat-set → nat-set |
| ∪ | nat-set | function,
nat-set × nat-set → nat-set |
| ∪ | key-list-set | function,
key-set × key-set → key-set |
| ∪ | address-store | function,
address-set × address-set → address-set |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | address-list-set | predicate,
address-set × address-set |
| ⊆ | node-store | predicate,
address-set × address-set |
| ⊆ | node-store | predicate,
node-store × node-store |
| ⊆ | node-index | predicate,
key-set × key-set |
| ⊆ | node-index | predicate,
node-index × node-index |
| ⊆ | set-basic | predicate,
set × set |
| ⊆ | store | predicate,
store × store |
| ⊆ | nat-list-set | predicate,
nat-set × nat-set |
| ⊆ | group-store | predicate,
group-address-store × group-address-store |
| ⊆ | group-store | predicate,
group-store × group-store |
| ⊆ | index-store | predicate,
index-address-store × index-address-store |
| ⊆ | index-store | predicate,
index-store × index-store |
| ⊆ | stringset | predicate,
stringset × stringset |
| ⊆ | nat-store | predicate,
nat-set × nat-set |
| ⊆ | nat-set | predicate,
nat-set × nat-set |
| ⊆ | key-list-set | predicate,
key-set × key-set |
| ⊆ | address-store | predicate,
address-set × address-set |
| ⊆ | address-store | predicate,
address-store × address-store |
| ⊏ | string | predicate,
string × string |
| ⊑ | address-list-set | predicate,
address-list × address-list |
| ⊑ | list-last | predicate,
list × list |
| ⊑ | nat-list-set | predicate,
nat-list × nat-list |
| ⊑ | group-store | predicate,
group-store × group-store |
| ⊑ | group-store | predicate,
group-node-list × group-node-list |
| ⊑ | index-store | predicate,
index-store × index-store |
| ⊑ | index-store | predicate,
index-node-list × index-node-list |
| ⊑ | ablock-store-inv | predicate,
store × store |
| ⊑ | key-list-set | predicate,
key-list × key-list |
| ⊑ | laddress-list | predicate,
laddress-list × laddress-list |
| ⊑ | node-list | predicate,
node-list × node-list |
| ⊑ | string | predicate,
string × string |
| ⊒ | address-list-set | predicate,
address-list × address-list |
| ⊒ | list-last | predicate,
list × list |
| ⊒ | nat-list-set | predicate,
nat-list × nat-list |
| ⊒ | group-store | predicate,
group-node-list × group-node-list |
| ⊒ | index-store | predicate,
index-node-list × index-node-list |
| ⊒ | key-list-set | predicate,
key-list × key-list |
| ⊒ | laddress-list | predicate,
laddress-list × laddress-list |
| ⊒ | node-list | predicate,
node-list × node-list |
| ⊒ | string | predicate,
string × string |
| ⊕ | node-store | function,
node-store × node-store → node-store |
| ⊕ | node-index | function,
node-index × node-index → node-index |
| ⊕ | store+set | function,
store × store → store |
| ⊕ | group-store | function,
group-address-store × group-address-store → group-address-store |
| ⊕ | group-store | function,
group-store × group-store → group-store |
| ⊕ | index-store | function,
index-address-store × index-address-store → index-address-store |
| ⊕ | index-store | function,
index-store × index-store → index-store |
| ⊕ | address-store | function,
address-store × address-store → address-store |
| ⊖ | aubifs-base | function,
node-index × key-set → node-index |
| ⊖ | aubifs-base | function,
node-index × key → node-index |
| ⌋ | error-class | predicate,
error |