| Symbol | Specification | Kind | Type |
|---|
| # . | buffer | f | buffer → nat |
| # . | string | f | string → nat |
| # . | avolume | f | avolume → nat |
| # . | lp-array | f | lp-array → nat |
| # . | nat-set | f | nat-set → nat |
| # . | nat-list-set | f | nat-list → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | string | f | char → string |
| . ' | nat-list-set | f | nat → nat-list |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | string | f | string × char → string |
| . + . | avolume | f | avolume × avolume → avolume |
| . + . | string | f | string × string → string |
| . + . | nat-list-set | f | nat × nat-list → nat-list |
| . + . | string | f | char × string → string |
| . + . | nat-list-set | f | nat-list × nat-list → nat-list |
| . + . | nat-list-set | f | nat-list × nat → nat-list |
| . ++ . | string | f | string × char → string |
| . ++ . | nat-set | f | nat-set × nat → nat-set |
| . ++ . | nat-list-set | f | nat-list × nat → nat-list |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | nat-list-set | f | nat × nat → nat-list |
| . +2 . | string | f | char × char → string |
| . - . | 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 . | string | f | string × char → string |
| . -1l . | nat-list-set | f | nat-list × nat → nat-list |
| . -l . | nat-list-set | f | nat-list × nat → nat-list |
| . -l . | string | f | string × char → string |
| . -p . | string | f | string × nat → string |
| . -p . | nat-list-set | f | nat-list × nat → nat-list |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .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 ≠ ∅ |
| . .char1 | string | pf | string → char with λ str. str ≠ "" |
| . .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 ≠ [] |
| . .indexaddr | superblock | f | superblock → address |
| . .indexaddr:= . | superblock | f | superblock × address → superblock |
| . .indicesWhere ( . ) | lp-array | f | lp-array × (lprops → bool) × nat → nat-list |
| . .indicesWhere ( . ) | lp-array | f | lp-array × (lprops → bool) → nat-list |
| . .last | string | pf | string → char with λ str. str ≠ "" |
| . .last | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .leb | ref-node | f | ref-node → nat |
| . .leb:= . | ref-node | f | ref-node × nat → ref-node |
| . .log | superblock | f | superblock → nat |
| . .log:= . | superblock | f | superblock × nat → superblock |
| . .lpt | superblock | f | superblock → nat |
| . .lpt:= . | superblock | f | superblock × nat → superblock |
| . .main | superblock | f | superblock → nat |
| . .main:= . | superblock | f | superblock × nat → superblock |
| . .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 ≠ ∅ |
| . .maxino | superblock | f | superblock → nat |
| . .maxino:= . | superblock | f | superblock × nat → superblock |
| . .min | nat-set | pf | nat-set → nat with λ ns. ns ≠ ∅ |
| . .orph | superblock | f | superblock → nat |
| . .orph:= . | superblock | f | superblock × nat → superblock |
| . .orphsize | superblock | f | superblock → nat |
| . .orphsize:= . | superblock | f | superblock × nat → superblock |
| . .ref-size | lprops | f | lprops → nat |
| . .ref-size:= . | lprops | f | lprops × nat → lprops |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .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 |
| . .toString | debug | f | nat → string |
| . / . | 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 |
| . [ . ] | string | pf | string × nat × char → string with λ str, n, char. n < # str |
| . [ . ] | string | pf | string × nat → char with λ str, n. n < # str |
| . [ . ] | 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 |
| . ∈ . | string | p | char × string |
| . ∈ . | lp-array | p | lprops × lp-array |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | nat-list-set | p | nat × nat-list |
| . ∈ . | avolume | p | aleb × avolume |
| . ∈ . | nat-set | p | nat × nat-set |
| . ∩ . | 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 |
| . ⊑ . | string | p | string × string |
| . ⊑ . | nat-list-set | p | nat-list × nat-list |
| . ⊒ . | string | p | string × string |
| . ⊒ . | 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 |
| ⊏ | string | p | string × string |
| ⌊ . ⌋ | error-class | p | error |
| AVOL | ebm-avol-asm | v | avolume,flexible |
| BUF | apersistence-io-asm | v | buffer,flexible |
| BUF0 | apersistence-io-asm | v | buffer,flexible |
| Boolvar | encoding-superblock | v | bool,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 |
| ENCODED_LPROPS_SIZE | encoding-lprops | c | nat |
| ENCODED_NAT_SIZE | encoding-nat | c | nat |
| ENCODED_REF_NODE_SIZE | encoding-ref-node | c | nat |
| 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 |
| INDEXADR | persistence-io-asm | v | address,flexible |
| INDEXADR0 | persistence-io-asm | v | address,flexible |
| ISBUF | apersistence-io-asm | v | bool,flexible |
| LEB_SIZE | eraseblock | c | nat |
| LEBSIZE | persistence-io-asm | v | nat,flexible |
| LNUM | apersistence-io-asm | v | nat,flexible |
| LOG | apersistence-io-asm | v | nat-list,flexible |
| LOGOFF | persistence-io-asm | v | nat,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 |
| MAXINO | persistence-io-asm | v | nat,flexible |
| MAXINO0 | persistence-io-asm | v | nat,flexible |
| N | apersistence-io-asm | v | nat,flexible |
| N0 | apersistence-io-asm | v | nat,flexible |
| N1 | apersistence-io-asm | v | nat,flexible |
| NEWSB | persistence-io-asm | v | superblock,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 |
| PAGESIZE | persistence-io-asm | v | nat,flexible |
| 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 |
| RND | persistence-io-asm | v | ref-node,flexible |
| SB | persistence-io-asm | v | superblock,flexible |
| SB_LOG | persistence-io-inv | c | nat |
| SB_LPT | persistence-io-inv | c | nat |
| SB_ORPH | persistence-io-inv | c | nat |
| 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 | |
| boolvar | encoding-superblock | v | bool |
| boolvar0 | encoding-superblock | v | bool |
| boolvar1 | encoding-superblock | v | bool |
| buf | buffer | v | buffer |
| buf0 | buffer | v | buffer |
| buf1 | buffer | v | buffer |
| buf2 | buffer | v | buffer |
| buffer | buffer | s | |
| butlastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| butlastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| char | char | s | |
| char | char | v | char |
| char0 | char | v | char |
| char1 | char | v | char |
| char2 | char | v | char |
| 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 | buffer | pp | buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| cmp | avolume | pp | avolume × nat × avolume × nat × nat with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0 |
| 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 | |
| debug# | debug | pr | string : |
| decode_lprops# | encoding-lprops | pr | nat × buffer : lprops × nat : error (nondeterministic) |
| decode_nat# | encoding-nat | pr | nat × buffer : nat × nat : error (nondeterministic) |
| decode_ref_node# | encoding-ref-node | pr | nat × buffer : ref-node : error (nondeterministic) |
| decode_ref_node_empty# | encoding-ref-node | pr | nat × buffer : ref-node × nat : error (nondeterministic) |
| decode_ref_node_nonempty# | encoding-ref-node | pr | nat × buffer : ref-node : error (nondeterministic) |
| decode_superblock# | encoding-superblock | pr | nat × buffer × nat : superblock × nat : error (nondeterministic) |
| decode_superblock_unaligned# | encoding-superblock | pr | nat × buffer : superblock × nat : error (nondeterministic) |
| disj | nat-list-set | p | nat-list × nat-list |
| disj | string | p | string × string |
| disk-layout | persistence-io-inv | p | superblock × nat |
| dropn | nat-list-set | f | nat × nat-list → nat-list |
| dups | string | p | string |
| dups | nat-list-set | p | nat-list |
| ebm-vol-inv | ebm-vol-inv | p | avolume |
| ebm_avol_change# | ebm-avol-asm | pr | nat × nat × buffer : avolume : error (nondeterministic) |
| ebm_avol_format# | ebm-avol-asm | pr | nat : : avolume × error (nondeterministic) |
| ebm_avol_get_leb_size# | ebm-avol-asm | pr | avolume : : nat |
| ebm_avol_get_page_size# | ebm-avol-asm | pr | avolume : : nat |
| ebm_avol_get_volume_size# | ebm-avol-asm | pr | avolume : : nat |
| ebm_avol_read# | ebm-avol-asm | pr | nat × nat × nat × nat × avolume : buffer : error (nondeterministic) |
| ebm_avol_recover# | ebm-avol-asm | pr | : avolume : error (nondeterministic) |
| ebm_avol_remap# | ebm-avol-asm | pr | nat : avolume : error (nondeterministic) |
| ebm_avol_sync_device# | ebm-avol-asm | pr | avolume : : error (nondeterministic) |
| ebm_avol_unmap# | ebm-avol-asm | pr | nat : avolume (nonfunctional) |
| ebm_avol_write# | ebm-avol-asm | pr | nat × nat × nat × nat × buffer : avolume : error (nondeterministic) |
| empty | buffer | c | data |
| empty | avolume | c | aleb |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| encode_lprops# | encoding-lprops | pr | lprops × nat : buffer × nat : error (nondeterministic) |
| encode_nat# | encoding-nat | pr | nat × nat : buffer × nat : error (nondeterministic) |
| encode_ref_node# | encoding-ref-node | pr | nat × ref-node : buffer : error (nondeterministic) |
| encode_ref_node_empty# | encoding-ref-node | pr | ref-node × nat : buffer × nat : error (nondeterministic) |
| encode_ref_node_nonempty# | encoding-ref-node | pr | ref-node × nat : buffer : error (nondeterministic) |
| encode_superblock# | encoding-superblock | pr | superblock × nat × nat : buffer × nat : error (nondeterministic) |
| encode_superblock_unaligned# | encoding-superblock | pr | superblock × nat : buffer × nat : error (nondeterministic) |
| encoding-size | encoding-superblock | f | superblock × nat → nat |
| encoding-size | encoding-nat | f | nat → nat |
| encoding-size | encoding-lprops | f | lprops → nat |
| encoding-size | encoding-ref-node | f | ref-node → nat |
| encoding-size-unaligned | encoding-superblock | f | superblock → nat |
| 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 | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fill | lp-array | f | lp-array × lprops → lp-array |
| fillfirst | nat-list-set | f | nat × nat × nat-list → nat-list |
| fillfirst | string | f | nat × char × string → string |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| 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 |
| frome | string | f | string × char → string |
| 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 |
| is-encoded | encoding-superblock | p | superblock × buffer |
| is-encoded | encoding-orphans | p | nat-set × buffer |
| is-encoded | encoding-lprops | p | lprops × buffer |
| is-encoded | encoding-nat | p | nat × buffer |
| is-encoded | encoding-lpt | p | lp-array × buffer × nat |
| is-encoded | encoding-log | p | nat-list × buffer |
| is-encoded | encoding-lpt | p | lp-array × buffer |
| is-encoded | encoding-ref-node | p | ref-node × buffer |
| is-encoded-empty | encoding-ref-node | p | ref-node × buffer |
| is-encoded-nonempty | encoding-ref-node | p | ref-node × buffer |
| is-encoded-pad | encoding-orphans | p | nat-set × nat × buffer |
| is-encoded-unaligned | encoding-superblock | p | superblock × buffer |
| is-garbage-lprops | encoding-lprops | p | buffer |
| is-garbage-nat | encoding-nat | p | buffer |
| is-garbage-rnode | encoding-ref-node | p | buffer |
| is-garbage-rnode-empty | encoding-ref-node | p | buffer |
| is-garbage-rnode-nonempty | encoding-ref-node | p | buffer |
| is-garbage-sb-unaligned | encoding-superblock | p | buffer |
| isbuf | apersistence-io-asm | v | bool |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| lastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| lastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| lebs | persistence-io-inv | f | avolume × nat × nat → buffer |
| log | apersistence-io-asm | v | nat-list |
| logoff | persistence-io-inv | v | nat |
| 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 |
| lptlebs | encoding-lpt | f | nat × nat → nat |
| lptsize | encoding-lpt | f | nat × nat → nat |
| m | nat-basic | v | nat |
| m0 | array-copy | v | nat |
| m1 | lprops | v | nat |
| m10 | superblock | v | nat |
| m2 | lprops | v | nat |
| m3 | lprops | v | nat |
| m4 | lprops | v | nat |
| m5 | superblock | v | nat |
| m6 | superblock | v | nat |
| m7 | superblock | v | nat |
| m8 | superblock | v | nat |
| m9 | superblock | v | nat |
| main | persistence-io-inv | v | nat |
| mainareasize | encoding-lpt | v | nat |
| mapped | aleb | f | buffer → aleb |
| mapped-full? | persistence-io-inv | p | avolume × nat × nat |
| 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 | string | f | char × nat → string |
| mklist | nat-list-set | f | nat × nat → nat-list |
| mklp | lprops | f | nat × nat × lpropflags × nat → lprops |
| mklparray | lp-array | f | nat → lp-array |
| mksb | superblock | f | address × nat × nat × nat × nat × nat × nat → superblock |
| 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 |
| orphans | persistence-io-inv | v | nat-set |
| persistence-io-inv | persistence-io-inv | p | superblock × nat × avolume × lp-array × nat-list × nat-set |
| persistence_io_add_log_leb# | persistence-io-asm | pr | nat × superblock × nat × nat : nat × avolume : error (nondeterministic) |
| persistence_io_commit# | persistence-io-asm | pr | lp-array × address × nat × nat × nat
: nat-set × superblock × avolume × nat
: error (nondeterministic) |
| persistence_io_decode_lpt# | persistence-io-asm | pr | buffer : lp-array × error (nondeterministic nonfunctional) |
| persistence_io_decode_orphans# | persistence-io-asm | pr | nat × buffer : : nat-set × error (nondeterministic) |
| persistence_io_encode_lpt# | persistence-io-asm | pr | lp-array × nat : : buffer × error (nondeterministic) |
| persistence_io_encode_orphans# | persistence-io-asm | pr | nat × nat : nat-set × buffer : error (nondeterministic) |
| persistence_io_format# | persistence-io-asm | pr | nat × nat × lp-array × address × nat
: superblock × nat × nat × avolume
: nat × error (nondeterministic) |
| persistence_io_get_leb_size# | persistence-io-asm | pr | nat : : nat |
| persistence_io_get_page_size# | persistence-io-asm | pr | nat : : nat |
| persistence_io_get_volume_size# | persistence-io-asm | pr | superblock × avolume : : nat |
| persistence_io_read# | persistence-io-asm | pr | nat × nat × nat × nat × superblock × avolume : buffer : error (nondeterministic) |
| persistence_io_read_lebs# | persistence-io-asm | pr | nat × nat × nat × avolume : : buffer × error (nondeterministic) |
| persistence_io_read_log# | persistence-io-asm | pr | superblock × nat × nat × avolume : nat : nat-list × error (nondeterministic) |
| persistence_io_read_orphans# | persistence-io-asm | pr | superblock × avolume : nat-set : error (nondeterministic) |
| persistence_io_read_superblock# | persistence-io-asm | pr | nat × nat × avolume : superblock : error (nondeterministic) |
| persistence_io_recover# | persistence-io-asm | pr | : address × nat × nat-set × nat-list × lp-array × superblock × nat ×
nat × nat × avolume
: error (nondeterministic) |
| persistence_io_remap# | persistence-io-asm | pr | nat × superblock : avolume : error (nondeterministic) |
| persistence_io_requires_commit# | persistence-io-asm | pr | nat × nat : : bool |
| persistence_io_unmap# | persistence-io-asm | pr | nat × superblock : avolume (nonfunctional) |
| persistence_io_write# | persistence-io-asm | pr | nat × nat × nat × nat × buffer × superblock : avolume : error (nondeterministic) |
| persistence_io_write_lebs# | persistence-io-asm | pr | nat × nat × buffer × nat : avolume : error (nondeterministic) |
| persistence_io_write_orphans# | persistence-io-asm | pr | nat × nat × nat : nat-set × avolume : error (nondeterministic) |
| persistence_io_write_superblock# | persistence-io-asm | pr | superblock × nat × nat : avolume : error (nondeterministic) |
| plog | apersistence-io-asm | v | nat-list |
| pos | nat-list-set | f | nat × nat-list → nat |
| pos | string | f | char × string → 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 |
| ref-node | ref-node | s | |
| resize | avolume | f | avolume × nat → avolume |
| resize | buffer | f | buffer × nat → buffer |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| 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 | string | f | string → string |
| rev | nat-list-set | f | nat-list → nat-list |
| rev | lp-array | f | lp-array → lp-array |
| rmdup | nat-list-set | f | nat-list → nat-list |
| rmdup | string | f | string → string |
| rnd | ref-node | v | ref-node |
| rnd0 | ref-node | v | ref-node |
| rnd1 | ref-node | v | ref-node |
| rnode | ref-node | f | nat → ref-node |
| sb | superblock | v | superblock |
| sb0 | superblock | v | superblock |
| sb1 | superblock | v | superblock |
| 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 |
| str | string | v | string |
| str0 | string | v | string |
| str1 | string | v | string |
| str2 | string | v | string |
| str3 | string | v | string |
| string | string | s | |
| 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 | string | pf | nat × nat × string → string with λ n, m, str. n + m ≤ # str |
| sublist | nat-list-set | pf | nat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx |
| superblock | superblock | s | |
| unmapped | aleb | c | aleb |
| valid-indices | lp-array | p | lp-array × nat-list |
| zero | buffer | c | data |
| zero | avolume | c | aleb |