| Symbol | Specification | Kind | Type |
|---|
| # . | buffer | f | buffer → nat |
| # . | lp-array | f | lp-array → nat |
| # . | avolume | f | avolume → nat |
| # . | nat-list-set | f | nat-list → nat |
| # . | nat-set | f | nat-set → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | nat-list-set | f | nat → nat-list |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | nat-list-set | f | nat-list × nat → nat-list |
| . + . | avolume | f | avolume × avolume → avolume |
| . + . | nat-list-set | f | nat-list × nat-list → nat-list |
| . + . | nat-list-set | f | nat × nat-list → nat-list |
| . ++ . | nat-list-set | f | nat-list × nat → nat-list |
| . ++ . | nat-set | f | nat-set × nat → nat-set |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | nat-list-set | f | nat × nat → nat-list |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | nat-set | f | nat-set × nat → nat-set |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | nat-list-set | f | nat-list × nat → nat-list |
| . -l . | nat-list-set | f | nat-list × nat → nat-list |
| . -p . | nat-list-set | f | nat-list × nat → nat-list |
| . .butlast | nat-list-set | pf | nat-list → nat-list with λ nx. nx ≠ [] |
| . .butmax | nat-set | pf | nat-set → nat-set with λ ns. ns ≠ ∅ |
| . .butmin | nat-set | pf | nat-set → nat-set with λ ns. ns ≠ ∅ |
| . .data | aleb | pf | aleb → buffer with λ aleb. aleb.mapped? |
| . .data:= . | aleb | pf | aleb × buffer → aleb with λ aleb, buf. aleb.mapped? |
| . .filter ( . ) | array-indices | f | nat-set × (nat → bool) → nat-set |
| . .flags | lprops | f | lprops → lpropflags |
| . .flags:= . | lprops | f | lprops × lpropflags → lprops |
| . .gcheapidx | lprops | f | lprops → nat |
| . .gcheapidx:= . | lprops | f | lprops × nat → lprops |
| . .head | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .indicesWhere ( . ) | lp-array | f | lp-array × (lprops → bool) → nat-list |
| . .indicesWhere ( . ) | lp-array | f | lp-array × (lprops → bool) × nat → nat-list |
| . .last | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .map ( . ) | lp-array | f | lp-array × (lprops → lprops) → lp-array |
| . .map ( . ) | array-indices | f | nat-set × (nat → nat) → nat-set |
| . .mapIf ( . ) | lp-array | f | lp-array × (lprops → bool) × (lprops → lprops) → lp-array |
| . .mapIf ( . ) | lp-array | f | lp-array × (lprops → bool) × (lprops → lprops) × nat → lp-array |
| . .mapIndices ( . ) | lp-array | f | lp-array × nat-list × (lprops → lprops) → lp-array |
| . .mapIndices ( . ) | lp-array | f | lp-array × nat-set × (lprops → lprops) → lp-array |
| . .mapped? | aleb | p | aleb |
| . .max | nat-set | pf | nat-set → nat with λ ns. ns ≠ ∅ |
| . .min | nat-set | pf | nat-set → nat with λ ns. ns ≠ ∅ |
| . .ref-size | lprops | f | lprops → nat |
| . .ref-size:= . | lprops | f | lprops × nat → lprops |
| . .size | lprops | f | lprops → nat |
| . .size:= . | lprops | f | lprops × nat → lprops |
| . .tail | nat-list-set | pf | nat-list → nat-list with λ nx. nx ≠ [] |
| . .toSet | nat-list-set | f | nat-list → nat-set |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . < . | nat-list-less | p | nat-list × nat |
| . < . | nat-list-set | p | nat-list × nat-list |
| . < . | nat-set | p | nat × nat-set |
| . < . | nat-set | p | nat-set × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | lp-array | pf | lp-array × nat × lprops → lp-array with λ lpt, n, lp. n < # lpt |
| . [ . ] | lp-array | pf | lp-array × nat → lprops with λ lpt, n. n < # lpt |
| . [ . ] | nat-list-set | pf | nat-list × nat × nat → nat-list with λ nx, n, n0. n < # nx |
| . [ . ] | nat-list-set | pf | nat-list × nat → nat with λ nx, n. n < # nx |
| . [ . ] | avolume | pf | avolume × nat × aleb → avolume with λ avol, n, aleb. n < # avol |
| . [ . ] | avolume | pf | avolume × nat → aleb with λ avol, n. n < # avol |
| . [ . ] | buffer | pf | buffer × nat × data → buffer with λ buf, n, d. n < # buf |
| . [ . ] | buffer | pf | buffer × nat → data with λ buf, n. n < # buf |
| . \ . | nat-set | f | nat-set × nat-set → nat-set |
| . ∈ . | lp-array | p | lprops × lp-array |
| . ∈ . | nat-list-set | p | nat × nat-list |
| . ∈ . | nat-set | p | nat × nat-set |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | avolume | p | aleb × avolume |
| . ∩ . | nat-set | f | nat-set × nat-set → nat-set |
| . ∪ . | nat-set | f | nat-set × nat-set → nat-set |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | ebm-vol-inv | p | avolume × avolume |
| . ⊆ . | nat-set | p | nat-set × nat-set |
| . ⊑ . | nat-list-set | p | nat-list × nat-list |
| . ⊒ . | nat-list-set | p | nat-list × nat-list |
| [] | nat-list-set | c | nat-list |
| { . } | nat-set | f | nat → nat-set |
| φ | lp-array | v | lprops → bool |
| φn | array-indices | v | nat → bool |
| ∅ | nat-set | c | nat-set |
| ⌊ . ⌋ | error-class | p | error |
| BUF | apersistence-io-asm | v | buffer,flexible |
| BUF0 | apersistence-io-asm | v | buffer,flexible |
| COMMIT? | apersistence-io-asm | v | bool,flexible |
| EACCESS | error | c | error |
| EB_PAGE_SIZE | eraseblock | c | nat |
| EBADFD | error | c | error |
| ECOMMIT | error | c | error |
| EEXISTS | error | c | error |
| EFAIL | error | c | error |
| EINVAL | error | c | error |
| EIO | error | c | error |
| EISDIR | error | c | error |
| ENOENT | error | c | error |
| ENOMEM | error | c | error |
| ENOSPC | error | c | error |
| ENOTDIR | error | c | error |
| ENOTEMPTY | error | c | error |
| EROFS | error | c | error |
| ERR | error-class | v | error,flexible |
| ERR0 | error-class | v | error,flexible |
| ESUCCESS | error | c | error |
| EUCLEAN | error | c | error |
| ISBUF | apersistence-io-asm | v | bool,flexible |
| LEB_SIZE | eraseblock | c | nat |
| LNUM | apersistence-io-asm | v | nat,flexible |
| LOG | apersistence-io-asm | v | nat-list,flexible |
| LP_FREE | lprops | c | lpropflags |
| LP_GROUP_NODES | lprops | c | lpropflags |
| LP_INDEX_NODES | lprops | c | lpropflags |
| LPT | apersistence-io-asm | v | lp-array,flexible |
| N | apersistence-io-asm | v | nat,flexible |
| N0 | apersistence-io-asm | v | nat,flexible |
| N1 | apersistence-io-asm | v | nat,flexible |
| OFFSET | apersistence-io-asm | v | nat,flexible |
| ORPHANS | apersistence-io-asm | v | nat-set,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PEB_SIZE | eraseblock | c | nat |
| PLOG | apersistence-io-asm | v | nat-list,flexible |
| PLPT | apersistence-io-asm | v | lp-array,flexible |
| PMAXINO | apersistence-io-asm | v | nat,flexible |
| PMAXINO0 | apersistence-io-asm | v | nat,flexible |
| PORPHANS | apersistence-io-asm | v | nat-set,flexible |
| PROOTADR | apersistence-io-asm | v | address,flexible |
| PROOTADR0 | apersistence-io-asm | v | address,flexible |
| PVOL | apersistence-io-asm | v | avolume,flexible |
| SIZE | apersistence-io-asm | v | nat,flexible |
| VOLSIZE | apersistence-io-asm | v | nat,flexible |
| address | address | s | |
| adr | address | v | address |
| adr0 | address | v | address |
| adr1 | address | v | address |
| adr2 | address | v | address |
| adr3 | address | v | address |
| adr4 | address | v | address |
| adr5 | address | v | address |
| aleb | aleb | s | |
| aleb | aleb | v | aleb |
| aleb0 | avolume | v | aleb |
| aleb1 | avolume | v | aleb |
| align↑ | align | f | nat × nat → nat |
| align↓ | align | f | nat × nat → nat |
| apersistence_io_add_log_leb# | apersistence-io-asm | pr | nat × address × nat × avolume × lp-array × nat-set : nat-list : error (nondeterministic) |
| apersistence_io_commit# | apersistence-io-asm | pr | lp-array × address × nat × avolume
: nat-set × address × nat × nat-list × lp-array × nat-set
: error (nondeterministic) |
| apersistence_io_format# | apersistence-io-asm | pr | nat × nat × lp-array × address × nat
:
: address × nat × nat-list × avolume × lp-array × nat-set × error (nondeterministic) |
| apersistence_io_get_leb_size# | apersistence-io-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_get_page_size# | apersistence-io-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_get_volume_size# | apersistence-io-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_read# | apersistence-io-asm | pr | nat × nat × nat × nat × address × nat × nat-list × avolume × lp-array ×
nat-set
: buffer
: error (nondeterministic) |
| apersistence_io_recover# | apersistence-io-asm | pr | : address × nat × nat-set × nat-list × lp-array × address × nat ×
nat-list × lp-array × nat-set × avolume
: error (nondeterministic) |
| apersistence_io_remap# | apersistence-io-asm | pr | nat × address × nat × nat-list × lp-array × nat-set : avolume : error (nondeterministic) |
| apersistence_io_requires_commit# | apersistence-io-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : bool (nondeterministic) |
| apersistence_io_unmap# | apersistence-io-asm | pr | nat × address × nat × nat-list × lp-array × nat-set : avolume (nonfunctional) |
| apersistence_io_write# | apersistence-io-asm | pr | nat × nat × nat × nat × buffer × address × nat × nat-list × lp-array ×
nat-set
: avolume
: error (nondeterministic) |
| avol | avolume | v | avolume |
| avol0 | avolume | v | avolume |
| avol1 | avolume | v | avolume |
| avol2 | avolume | v | avolume |
| avolume | avolume | s | |
| buf | buffer | v | buffer |
| buf0 | buffer | v | buffer |
| buf1 | buffer | v | buffer |
| buf2 | buffer | v | buffer |
| buffer | buffer | s | |
| butlastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| cmp | lp-array | pp | lp-array × lprops × nat × nat with λ lpt, lp, m, n. m + n ≤ # lpt |
| cmp | lp-array | pp | lp-array × nat × lp-array × nat × nat with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0 |
| cmp | avolume | pp | avolume × aleb × nat × nat with λ avol, aleb, m, n. m + n ≤ # avol |
| cmp | avolume | pp | avolume × nat × avolume × nat × nat with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| cmp | buffer | pp | buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| cmp | buffer | pp | buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | lp-array | pf | lp-array × nat × lp-array × nat × nat → lp-array with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0 |
| copy | avolume | pf | avolume × nat × avolume × nat × nat → avolume with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| d | data | v | data |
| d0 | data | v | data |
| d1 | data | v | data |
| d2 | data | v | data |
| data | data | s | |
| disj | nat-list-set | p | nat-list × nat-list |
| dropn | nat-list-set | f | nat × nat-list → nat-list |
| dups | nat-list-set | p | nat-list |
| ebm-vol-inv | ebm-vol-inv | p | avolume |
| empty | buffer | c | data |
| empty | avolume | c | aleb |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| err | error | v | error |
| err0 | error | v | error |
| err1 | error | v | error |
| error | error | s | |
| fail# | error-class | pr | : : error (nondeterministic) |
| fail_or_success# | error-class | pr | : : error (nondeterministic) |
| fill | buffer | f | buffer × data → buffer |
| fill | lp-array | pf | lp-array × lprops × nat × nat → lp-array with λ lpt, lp, n, m. n + m ≤ # lpt |
| fill | avolume | f | avolume × aleb → avolume |
| fill | avolume | pf | avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol |
| fill | lp-array | f | lp-array × lprops → lp-array |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fillfirst | nat-list-set | f | nat × nat × nat-list → nat-list |
| firstn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| fn | array-indices | v | nat → nat |
| frome | nat-list-set | f | nat-list × nat → nat-list |
| id○ | lp-array | p | lp-array × lp-array × nat |
| id○ | buffer | p | buffer × buffer × nat |
| id○ | avolume | p | avolume × avolume × nat |
| idrange | lp-array | pp | lp-array × nat × nat with λ lpt, m, n. m + n ≤ # lpt |
| idrange | avolume | pp | avolume × nat × nat with λ avol, m, n. m + n ≤ # avol |
| idrange | buffer | pp | buffer × nat × nat with λ buf, m, n. m + n ≤ # buf |
| is-aligned | align | p | nat × nat |
| isbuf | apersistence-io-asm | v | bool |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| lastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| log | apersistence-io-asm | v | nat-list |
| lp | lprops | v | lprops |
| lp-array | lp-array | s | |
| lp0 | lprops | v | lprops |
| lp1 | lp-array | v | lprops |
| lpf | lprops | v | lpropflags |
| lpf0 | lprops | v | lpropflags |
| lpropflags | lprops | s | |
| lprops | lprops | s | |
| lpt | lp-array | v | lp-array |
| lpt0 | lp-array | v | lp-array |
| lpt1 | lp-array | v | lp-array |
| lpt2 | lp-array | v | lp-array |
| lptfun | lp-array | v | lprops → lprops |
| m | nat-basic | v | nat |
| m0 | array-copy | v | nat |
| m1 | lprops | v | nat |
| m2 | lprops | v | nat |
| m3 | lprops | v | nat |
| m4 | lprops | v | nat |
| mapped | aleb | f | buffer → aleb |
| max | min-max | f | nat × nat → nat |
| min | min-max | f | nat × nat → nat |
| mkavolume | avolume | f | nat → avolume |
| mkbuf | buffer | f | nat → buffer |
| mkemparray | avolume | f | nat → avolume |
| mkempbuf | buffer | f | nat → buffer |
| mklist | nat-list-set | f | nat × nat → nat-list |
| mklp | lprops | f | nat × nat × lpropflags × nat → lprops |
| mklparray | lp-array | f | nat → lp-array |
| mkzarray | avolume | f | nat → avolume |
| mkzbuf | buffer | f | nat → buffer |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| n2 | nat-set | v | nat |
| n3 | nat-set | v | nat |
| n4 | nat-set | v | nat |
| n5 | nat-list-set | v | nat |
| nat | nat-basic | s | |
| nat-list | nat-list-set | s | |
| nat-set | nat-set | s | |
| ns | nat-set | v | nat-set |
| ns0 | nat-set | v | nat-set |
| ns1 | nat-set | v | nat-set |
| ns2 | nat-set | v | nat-set |
| nx | nat-list-set | v | nat-list |
| nx0 | nat-list-set | v | nat-list |
| nx1 | nat-list-set | v | nat-list |
| ny | nat-list-set | v | nat-list |
| nz | nat-list-set | v | nat-list |
| plog | apersistence-io-asm | v | nat-list |
| pos | nat-list-set | f | nat × nat-list → nat |
| prefixn | nat-list-set | f | nat × nat-list → nat-list |
| range= | avolume | p | avolume × nat × avolume × nat × nat |
| range= | buffer | p | buffer × nat × buffer × nat × nat |
| resize | buffer | f | buffer × nat → buffer |
| resize | avolume | f | avolume × nat → avolume |
| restn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| rev | lp-array | pf | lp-array × nat → lp-array with λ lpt, n. n ≤ # lpt |
| rev | buffer | f | buffer → buffer |
| rev | avolume | pf | avolume × nat → avolume with λ avol, n. n ≤ # avol |
| rev | buffer | pf | buffer × nat → buffer with λ buf, n. n ≤ # buf |
| rev | avolume | f | avolume → avolume |
| rev | lp-array | f | lp-array → lp-array |
| rev | nat-list-set | f | nat-list → nat-list |
| rmdup | nat-list-set | f | nat-list → nat-list |
| slice | nat-list-set | f | nat × nat × nat-list → nat-list |
| splice | buffer | f | buffer × nat × buffer × nat × nat → buffer |
| splice | avolume | f | avolume × nat × avolume × nat × nat → avolume |
| subarray | lp-array | pf | lp-array × nat × nat → lp-array with λ lpt, m, n. m + n ≤ # lpt |
| subarray | buffer | pf | buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf |
| subarray | avolume | pf | avolume × nat × nat → avolume with λ avol, m, n. m + n ≤ # avol |
| sublist | nat-list-set | pf | nat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx |
| unmapped | aleb | c | aleb |
| valid-indices | lp-array | p | lp-array × nat-list |
| zero | buffer | c | data |
| zero | avolume | c | aleb |