| 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 |
| . .align↓ | awbuf-inv | f | avolume → avolume |
| . .align↓ | awbuf-inv | f | buffer → buffer |
| . .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 ≠ ∅ |
| . .content | wbuf | f | wbuf → buffer |
| . .content:= . | wbuf | f | wbuf × buffer → wbuf |
| . .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 |
| . .isbuf? | bufleb | p | bufleb |
| . .last | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .leb | bufleb | pf | bufleb → nat with λ bleb. bleb.isbuf? |
| . .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 ≠ ∅ |
| . .nbytes | wbuf | f | wbuf → nat |
| . .nbytes:= . | wbuf | f | wbuf × nat → wbuf |
| . .offset | wbuf | f | wbuf → nat |
| . .offset:= . | wbuf | f | wbuf × nat → wbuf |
| . .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 |
| . ↓ . | awbuf-inv | p | aleb × aleb |
| . ↓ . | awbuf-inv | p | avolume × avolume |
| . ∈ . | 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 |
| . ⊑ . | 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 |
| AROFS | awbuf-asm | v | bool,flexible |
| AROFS0 | awbuf-asm | v | bool,flexible |
| BEGINBUF | wbuf-asm | v | nat,flexible |
| BEGINWBUF | wbuf-asm | v | nat,flexible |
| BUF | awbuf-asm | v | buffer,flexible |
| BUF0 | awbuf-asm | v | buffer,flexible |
| BUFLEB | wbuf-asm | v | bufleb,flexible |
| BUFLEB0 | wbuf-asm | v | bufleb,flexible |
| COMMIT? | awbuf-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 | awbuf-asm | v | bool,flexible |
| LEB_SIZE | eraseblock | c | nat |
| LNUM | awbuf-asm | v | nat,flexible |
| LOG | awbuf-asm | v | nat-list,flexible |
| LP_FREE | lprops | c | lpropflags |
| LP_GROUP_NODES | lprops | c | lpropflags |
| LP_INDEX_NODES | lprops | c | lpropflags |
| LPT | awbuf-asm | v | lp-array,flexible |
| N | awbuf-asm | v | nat,flexible |
| N0 | awbuf-asm | v | nat,flexible |
| N1 | awbuf-asm | v | nat,flexible |
| N2 | wbuf-asm | v | nat,flexible |
| OFFSET | awbuf-asm | v | nat,flexible |
| ORPHANS | awbuf-asm | v | nat-set,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PAGESIZE | wbuf-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 |
| ROFS | wbuf-asm | v | bool,flexible |
| ROFS0 | wbuf-asm | v | bool,flexible |
| SIZE | awbuf-asm | v | nat,flexible |
| VOLSIZE | awbuf-asm | v | nat,flexible |
| WBUF | wbuf-asm | v | wbuf,flexible |
| WBUFLEB | awbuf-asm | v | bufleb,flexible |
| WBUFLEB0 | awbuf-asm | v | bufleb,flexible |
| WLOG | awbuf-asm | v | nat-list,flexible |
| WLPT | awbuf-asm | v | lp-array,flexible |
| WMAXINO | awbuf-asm | v | nat,flexible |
| WMAXINO0 | awbuf-asm | v | nat,flexible |
| WORPHANS | awbuf-asm | v | nat-set,flexible |
| WROOTADR | awbuf-asm | v | address,flexible |
| WROOTADR0 | awbuf-asm | v | address,flexible |
| WVOL | awbuf-asm | v | avolume,flexible |
| abs | wbuf-abs | p | avolume × bufleb × wbuf × avolume × bool |
| abs⊕ | wbuf-abs | f | aleb × wbuf → aleb |
| 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 | |
| awbuf-inv | awbuf-inv | p | avolume × bufleb |
| awbuf_add_log_leb# | awbuf-asm | pr | nat × nat × address × nat × avolume × lp-array × nat-set × bool
: nat-list × bufleb
: error (nondeterministic) |
| awbuf_commit# | awbuf-asm | pr | lp-array × address × nat × avolume × bufleb
: nat-set × address × nat × nat-list × lp-array × nat-set × bool
: error (nondeterministic) |
| awbuf_destroy_buf# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bool
: bufleb
: error |
| awbuf_enter_readonly# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb
:
: bool |
| awbuf_format# | awbuf-asm | pr | nat × nat × lp-array × address × nat
:
: address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool × error (nondeterministic) |
| awbuf_get_buf# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bufleb |
| awbuf_get_leb_size# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_page_size# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_volume_size# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_is_readonly# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| awbuf_move_buf# | awbuf-asm | pr | nat × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bool
: bufleb
: error (nondeterministic) |
| awbuf_read_buf# | awbuf-asm | pr | nat × nat × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
: buffer
: error (nondeterministic) |
| awbuf_recover# | awbuf-asm | pr | : address × nat × nat-set × nat-list × lp-array × address × nat ×
nat-list × lp-array × nat-set × avolume
: bufleb × bool × error (nondeterministic) |
| awbuf_remap# | awbuf-asm | pr | nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume
: error (nondeterministic) |
| awbuf_requires_commit# | awbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool (nondeterministic) |
| awbuf_unmap# | awbuf-asm | pr | nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume (nonfunctional) |
| awbuf_write_buf# | awbuf-asm | pr | nat × buffer × address × nat × nat-list × lp-array × nat-set × bufleb
: avolume × bool
: error (nondeterministic) |
| bleb | bufleb | v | bufleb |
| buf | buffer | v | buffer |
| buf0 | buffer | v | buffer |
| buf1 | buffer | v | buffer |
| buf2 | buffer | v | buffer |
| buffer | buffer | s | |
| buffered | bufleb | f | nat → bufleb |
| bufleb | bufleb | 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 | 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 | |
| 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 | lp-array | pf | lp-array × lprops × nat × nat → lp-array with λ lpt, lp, n, m. n + m ≤ # lpt |
| fill | buffer | f | buffer × data → buffer |
| 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 |
| 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 | awbuf-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 | bufleb | 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 |
| mkwbuf | wbuf | f | buffer × nat × nat → wbuf |
| 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 | |
| nobuffer | bufleb | c | bufleb |
| 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 |
| rofs | wbuf-base | v | bool |
| 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 |
| synced | awbuf-inv | p | avolume |
| unmapped | aleb | c | aleb |
| valid-indices | lp-array | p | lp-array × nat-list |
| wbuf | wbuf | s | |
| wbuf | wbuf | v | wbuf |
| wbuf-cons | wbuf-base | p | bufleb × wbuf × avolume × bool |
| wbuf-cons | wbuf-base | p | wbuf × aleb × bool |
| wbuf_add_log_leb# | wbuf-asm | pr | nat × nat × bool × address × nat × avolume × lp-array × nat-set
: bufleb × wbuf × nat-list
: error (nondeterministic) |
| wbuf_commit# | wbuf-asm | pr | lp-array × address × nat × avolume
: nat-set × address × nat × nat-list × lp-array × nat-set × bool
: error (nondeterministic) |
| wbuf_destroy_buf# | wbuf-asm | pr | bool : bufleb : error |
| wbuf_enter_readonly# | wbuf-asm | pr | : : bool |
| wbuf_format# | wbuf-asm | pr | nat × nat × lp-array × address × nat
: wbuf × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bufleb × bool
: error (nondeterministic) |
| wbuf_get_buf# | wbuf-asm | pr | bufleb : : bufleb |
| wbuf_get_leb_size# | wbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| wbuf_get_page_size# | wbuf-asm | pr | nat : : nat |
| wbuf_get_volume_size# | wbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| wbuf_is_readonly# | wbuf-asm | pr | bool : : bool |
| wbuf_move_buf# | wbuf-asm | pr | nat × nat × bool × avolume : bufleb × wbuf : error |
| wbuf_read_buf# | wbuf-asm | pr | nat × nat × nat × bufleb × wbuf × address × nat × nat-list × avolume ×
lp-array × nat-set
: buffer
: error (nondeterministic) |
| wbuf_recover# | wbuf-asm | pr | : address × nat × nat-set × nat-list × lp-array × wbuf × nat × address ×
nat × nat-list × avolume × lp-array × nat-set × bufleb × bool
: error (nondeterministic) |
| wbuf_remap# | wbuf-asm | pr | nat × bufleb × address × nat × nat-list × lp-array × nat-set
: avolume
: error (nondeterministic) |
| wbuf_requires_commit# | wbuf-asm | pr | address × nat × nat-list × avolume × lp-array × nat-set : : bool (nondeterministic) |
| wbuf_unmap# | wbuf-asm | pr | nat × bufleb × address × nat × nat-list × lp-array × nat-set : avolume (nonfunctional) |
| wbuf_write_buf# | wbuf-asm | pr | nat × buffer × bufleb × nat × address × nat × nat-list × lp-array ×
nat-set
: wbuf × bool × avolume
: error (nondeterministic) |
| zero | buffer | c | data |
| zero | avolume | c | aleb |