| Symbol | Specification | Kind | Type |
|---|
| # . | nat-list-set | f | nat-list → nat |
| # . | abstract-volumes | f | abstract-volumes → nat |
| # . | nat-set | f | nat-set → nat |
| # . | abstract-volume | f | abstract-volume → nat |
| # . | wlarray-base | f | wlarray → nat |
| # . | lebrefset | f | lebrefset → nat |
| # . | nat-bag | f | nat-bag → nat |
| # . | erasequeue-base | f | queue → nat |
| # . | buffer | f | buffer → nat |
| # . | volumes | f | volumes → nat |
| # . | apebs | f | apebs → nat |
| # . | ebatbl | f | ebatbl → nat |
| # . | vtbl | f | vtbl → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | erasequeue-base | f | erasequeueentry → queue |
| . ' | nat-list-set | f | nat → nat-list |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | nat-list-set | f | nat × nat-list → nat-list |
| . + . | erasequeue-base | f | queue × erasequeueentry → queue |
| . + . | nat-list-set | f | nat-list × nat-list → nat-list |
| . + . | erasequeue-base | f | queue × queue → queue |
| . + . | nat-list-set | f | nat-list × nat → nat-list |
| . + . | erasequeue-base | f | erasequeueentry × queue → queue |
| . + . | buffer | f | buffer × buffer → buffer |
| . ++ . | lebrefset | f | lebrefset × lebref → lebrefset |
| . ++ . | nat-list-set | f | nat-list × nat → nat-list |
| . ++ . | erasequeue-base | f | queue × erasequeueentry → queue |
| . ++ . | nat-set | f | nat-set × nat → nat-set |
| . ++ . | nat-bag | f | nat-bag × nat → nat-bag |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | nat-list-set | f | nat × nat → nat-list |
| . +2 . | erasequeue-base | f | erasequeueentry × erasequeueentry → queue |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . - . | erasequeue | f | queue × volid → queue |
| . - . | erasequeue | f | queue × nat → queue |
| . - . | erasequeue | f | queue × lebref → queue |
| . -- . | nat-set | f | nat-set × nat → nat-set |
| . -- . | abstract-volumes | f | abstract-volumes × volid → abstract-volumes |
| . -- . | nat-bag | f | nat-bag × nat → nat-bag |
| . -- . | lebrefset | f | lebrefset × lebref → lebrefset |
| . -- . | vtbl | f | vtbl × volid → vtbl |
| . -- . | volumes | f | volumes × volid → volumes |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | nat-list-set | f | nat-list × nat → nat-list |
| . -1l . | erasequeue-base | f | queue × erasequeueentry → queue |
| . -l . | nat-list-set | f | nat-list × nat → nat-list |
| . -l . | erasequeue-base | f | queue × erasequeueentry → queue |
| . -p . | nat-list-set | f | nat-list × nat → nat-list |
| . -p . | erasequeue-base | f | queue × nat → queue |
| . .bad | apeb | p | apeb |
| . .bad:= . | apeb | f | apeb × bool → apeb |
| . .butlast | erasequeue-base | pf | queue → queue with λ q. q ≠ [] |
| . .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 ≠ ∅ |
| . .checksum | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .checksum:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .data | leb | pf | leb → buffer with λ leb. leb.mapped? |
| . .data | apeb | f | apeb → buffer |
| . .data:= . | leb | pf | leb × buffer → leb with λ leb, buf. leb.mapped? |
| . .data:= . | apeb | f | apeb × buffer → apeb |
| . .ec | wlentry | f | wlentry → nat |
| . .ec | aecheader | pf | aecheader → nat with λ aehdr. aehdr.valid? |
| . .ec:= . | wlentry | f | wlentry × nat → wlentry |
| . .ec:= . | aecheader | pf | aecheader × nat → aecheader with λ aehdr, m. aehdr.valid? |
| . .echdr | apeb | f | apeb → aecheader |
| . .echdr:= . | apeb | f | apeb × aecheader → apeb |
| . .fill | leb | pf | leb → nat with λ leb. leb.mapped? |
| . .fill | apeb | f | apeb → nat |
| . .fill:= . | leb | pf | leb × nat → leb with λ leb, m. leb.mapped? |
| . .fill:= . | apeb | f | apeb × nat → apeb |
| . .filter ( . ) | array-indices | f | nat-set × (nat → bool) → nat-set |
| . .head | erasequeue-base | pf | queue → erasequeueentry with λ q. q ≠ [] |
| . .head | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .indicesWhere ( . ) | wlarray-base | f | wlarray × (wlentry → bool) → nat-list |
| . .indicesWhere ( . ) | wlarray-base | f | wlarray × (wlentry → bool) × nat → nat-list |
| . .last | erasequeue-base | pf | queue → erasequeueentry with λ q. q ≠ [] |
| . .last | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .leb | lebref | pf | lebref → nat with λ lref. lref ≠ none |
| . .leb | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .leb:= . | lebref | pf | lebref × nat → lebref with λ lref, m. lref ≠ none |
| . .leb:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .lebref | erasequeueentry | f | erasequeueentry → lebref |
| . .lebref:= . | erasequeueentry | f | erasequeueentry × lebref → erasequeueentry |
| . .lebrefs | erasequeue | f | queue → lebrefset |
| . .map ( . ) | array-indices | f | nat-set × (nat → nat) → nat-set |
| . .map ( . ) | wlarray-base | f | wlarray × (wlentry → wlentry) → wlarray |
| . .mapIf ( . ) | wlarray-base | f | wlarray × (wlentry → bool) × (wlentry → wlentry) → wlarray |
| . .mapIf ( . ) | wlarray-base | f | wlarray × (wlentry → bool) × (wlentry → wlentry) × nat → wlarray |
| . .mapIndices ( . ) | wlarray-base | f | wlarray × nat-list × (wlentry → wlentry) → wlarray |
| . .mapIndices ( . ) | wlarray-base | f | wlarray × nat-set × (wlentry → wlentry) → wlarray |
| . .mapped? | leb | p | leb |
| . .max | bag-max | f | nat-bag → nat |
| . .max | nat-set | pf | nat-set → nat with λ ns. ns ≠ ∅ |
| . .min | nat-set | pf | nat-set → nat with λ ns. ns ≠ ∅ |
| . .pnum | ebaentry | pf | ebaentry → nat with λ ebae. ebae ≠ unmapped |
| . .pnum | erasequeueentry | f | erasequeueentry → nat |
| . .pnum:= . | ebaentry | pf | ebaentry × nat → ebaentry with λ ebae, m. ebae ≠ unmapped |
| . .pnum:= . | erasequeueentry | f | erasequeueentry × nat → erasequeueentry |
| . .size | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .size:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .sqn | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .sqn:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .status | wlentry | f | wlentry → wlstatus |
| . .status:= . | wlentry | f | wlentry × wlstatus → wlentry |
| . .tail | erasequeue-base | pf | queue → queue with λ q. q ≠ [] |
| . .tail | nat-list-set | pf | nat-list → nat-list with λ nx. nx ≠ [] |
| . .toSet | nat-list-set | f | nat-list → nat-set |
| . .valid? | avidheader | p | avidheader |
| . .valid? | aecheader | p | aecheader |
| . .vidhdr | apeb | f | apeb → avidheader |
| . .vidhdr:= . | apeb | f | apeb × avidheader → apeb |
| . .vol | lebref | pf | lebref → volid with λ lref. lref ≠ none |
| . .vol | avidheader | pf | avidheader → volid with λ avhdr. avhdr.valid? |
| . .vol:= . | lebref | pf | lebref × volid → lebref with λ lref, v. lref ≠ none |
| . .vol:= . | avidheader | pf | avidheader × volid → avidheader with λ avhdr, v. avhdr.valid? |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . < . | erasequeue-base | p | queue × queue |
| . < . | nat-set | p | nat-set × nat |
| . < . | nat-list-set | p | nat-list × nat-list |
| . < . | nat-set | p | nat × nat-set |
| . < . | nat-list-less | p | nat-list × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | abstract-volumes | pf | abstract-volumes × volid → abstract-volume with λ avols, v. v ∈ avols |
| . [ . ] | abstract-volume | pf | abstract-volume × nat × leb → abstract-volume with λ evol, n, leb. n < # evol |
| . [ . ] | abstract-volume | pf | abstract-volume × nat → leb with λ evol, n. n < # evol |
| . [ . ] | erasequeue-base | pf | queue × nat × erasequeueentry → queue with λ q, n, eqent. n < # q |
| . [ . ] | erasequeue-base | pf | queue × nat → erasequeueentry with λ q, n. n < # q |
| . [ . ] | volumes | pf | volumes × volid → ebatbl with λ vols, v. v ∈ vols |
| . [ . ] | vtbl | f | vtbl × volid × nat → vtbl |
| . [ . ] | ebatbl | pf | ebatbl × nat × ebaentry → ebatbl with λ ebatbl, n, ebae. n < # ebatbl |
| . [ . ] | volumes | f | volumes × volid × ebatbl → volumes |
| . [ . ] | ebatbl | pf | ebatbl × nat → ebaentry with λ ebatbl, n. n < # ebatbl |
| . [ . ] | abstract-volumes | f | abstract-volumes × volid × abstract-volume → abstract-volumes |
| . [ . ] | vtbl | pf | vtbl × volid → nat with λ vtbl, v. v ∈ vtbl |
| . [ . ] | nat-list-set | pf | nat-list × nat → nat with λ nx, n. n < # nx |
| . [ . ] | apebs | pf | apebs × nat × apeb → apebs with λ apebs, n, apeb. n < # apebs |
| . [ . ] | nat-list-set | pf | nat-list × nat × nat → nat-list with λ nx, n, n0. n < # nx |
| . [ . ] | apebs | pf | apebs × nat → apeb with λ apebs, n. n < # apebs |
| . [ . ] | wlarray-base | pf | wlarray × nat → wlentry with λ wlar, n. n < # wlar |
| . [ . ] | buffer | pf | buffer × nat × data → buffer with λ buf, n, d. n < # buf |
| . [ . ] | wlarray-base | pf | wlarray × nat × wlentry → wlarray with λ wlar, n, wle. n < # wlar |
| . [ . ] | buffer | pf | buffer × nat → data with λ buf, n. n < # buf |
| . \ . | nat-set | f | nat-set × nat-set → nat-set |
| . \ . | nat-bag | f | nat-bag × nat-bag → nat-bag |
| . \ . | lebrefset | f | lebrefset × lebrefset → lebrefset |
| . \ . | erasequeue-base | f | queue × queue → queue |
| . × . | lebref | f | volid × nat → lebref |
| . ∈ . | abstract-volumes | p | volid × abstract-volumes |
| . ∈ . | nat-list-set | p | nat × nat-list |
| . ∈ . | abstract-volume | p | leb × abstract-volume |
| . ∈ . | nat-set | p | nat × nat-set |
| . ∈ . | erasequeue | p | volid × queue |
| . ∈ . | wlarray-base | p | wlentry × wlarray |
| . ∈ . | erasequeue | p | lebref × queue |
| . ∈ . | nat-bag | p | nat × nat-bag |
| . ∈ . | erasequeue | p | nat × queue |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | lebrefset | p | lebref × lebrefset |
| . ∈ . | apebs | p | apeb × apebs |
| . ∈ . | erasequeue-base | p | erasequeueentry × queue |
| . ∈ . | vtbl | p | volid × vtbl |
| . ∈ . | volumes | p | volid × volumes |
| . ∈ . | ebatbl | p | ebaentry × ebatbl |
| . ∩ . | nat-set | f | nat-set × nat-set → nat-set |
| . ∩ . | lebrefset | f | lebrefset × lebrefset → lebrefset |
| . ∪ . | nat-set | f | nat-set × nat-set → nat-set |
| . ∪ . | nat-bag | f | nat-bag × nat-bag → nat-bag |
| . ∪ . | vtbl | f | vtbl × vtbl → vtbl |
| . ∪ . | erasequeue-base | f | queue × queue → queue |
| . ∪ . | lebrefset | f | lebrefset × lebrefset → lebrefset |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | ebm-base | p | abstract-volumes × abstract-volumes |
| . ⊆ . | lebrefset | p | lebrefset × lebrefset |
| . ⊆ . | nat-set | p | nat-set × nat-set |
| . ⊆ . | erasequeue-base | p | queue × queue |
| . ⊆ . | nat-bag | p | nat-bag × nat-bag |
| . ⊆ . | vtbl | p | vtbl × vtbl |
| . ⊑ . | nat-list-set | p | nat-list × nat-list |
| . ⊑ . | erasequeue-base | p | queue × queue |
| . ⊒ . | nat-list-set | p | nat-list × nat-list |
| . ⊒ . | erasequeue-base | p | queue × queue |
| . ⊥ . | vtbl | p | vtbl × vtbl |
| . subseteq . | abstract-volumes | p | abstract-volumes × abstract-volumes |
| . subseteq . | volumes | p | volumes × volumes |
| [] | nat-list-set | c | nat-list |
| [] | erasequeue-base | c | queue |
| { . } | lebrefset | f | lebref → lebrefset |
| { . } | nat-set | f | nat → nat-set |
| { . } | nat-bag | f | nat → nat-bag |
| φn | array-indices | v | nat → bool |
| φwlentry | wlarray-base | v | wlentry → bool |
| ∅ | nat-set | c | nat-set |
| ∅ | nat-bag | c | nat-bag |
| ∅ | vtbl | c | vtbl |
| ∅ | abstract-volumes | c | abstract-volumes |
| ∅ | volumes | c | volumes |
| ∅ | lebrefset | c | lebrefset |
| ⌊ . ⌋ | error-class | p | error |
| ⌜ . ⌝ | ebaentry | f | nat → ebaentry |
| BUF | encoding-vtbl | v | buffer,flexible |
| Boolvar | encoding-nat | 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_NAT_SIZE | encoding-nat | c | nat |
| ENCODED_VOLID_SIZE | encoding-volid | 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 |
| INDEX | encoding-vtbl | v | nat,flexible |
| LEB_SIZE | eraseblock | c | nat |
| M | encoding-vtbl | v | nat,flexible |
| N | encoding-vtbl | v | nat,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PEB_SIZE | eraseblock | c | nat |
| SIZE | encoding-vtbl | v | nat,flexible |
| UBI_ERASE_RETRIES | ubi-base | c | nat |
| UBI_WRITE_RETRIES | ubi-base | c | nat |
| VOLID | encoding-vtbl | v | volid,flexible |
| VTBL | encoding-vtbl | v | vtbl,flexible |
| VTBL_LNUM | vtbl-conv | c | nat |
| VTBL_VOLID | vtbl-conv | c | volid |
| WL_THRESHOLD | ubi-base | c | nat |
| abs | ubi-abs | p | leb × apebs × ebaentry × queue |
| abs | ubi-abs | p | abstract-volumes × apebs × volumes × queue |
| abs○ | ubi-abs | p | abstract-volumes × apebs × volumes × queue × volid |
| abs○ | ubi-abs | p | abstract-volumes × apebs × volumes × queue × volid × nat |
| absf | ubi-abs | f | abstract-volumes × apebs × volumes × queue → abstract-volumes |
| absf | ubi-abs | f | volid × abstract-volume × apebs × ebatbl × queue × nat
→ abstract-volume |
| abstract-volume | abstract-volume | s | |
| abstract-volumes | abstract-volumes | s | |
| aechdr | aecheader | f | nat → aecheader |
| aecheader | aecheader | s | |
| aehdr | aecheader | v | aecheader |
| aehdr0 | aecheader | v | aecheader |
| aehdr1 | aecheader | v | aecheader |
| align↑ | align | f | nat × nat → nat |
| align↓ | align | f | nat × nat → nat |
| apeb | apeb | s | |
| apeb | apeb | v | apeb |
| apeb0 | apebs | v | apeb |
| apeb1 | apebs | v | apeb |
| apebs | apebs | s | |
| apebs | apebs | v | apebs |
| apebs0 | apebs | v | apebs |
| apebs1 | apebs | v | apebs |
| apebs2 | apebs | v | apebs |
| avhdr | avidheader | v | avidheader |
| avhdr0 | avidheader | v | avidheader |
| avhdr1 | avidheader | v | avidheader |
| avidhdr | avidheader | f | volid × nat × nat × nat × nat → avidheader |
| avidheader | avidheader | s | |
| avols | abstract-volumes | v | abstract-volumes |
| avols0 | abstract-volumes | v | abstract-volumes |
| avols1 | abstract-volumes | v | abstract-volumes |
| avols2 | abstract-volumes | v | abstract-volumes |
| bag | nat-bag | v | nat-bag |
| bag0 | nat-bag | v | nat-bag |
| bag1 | nat-bag | v | nat-bag |
| bag2 | nat-bag | v | nat-bag |
| below | wlarray | f | nat-set × nat → nat-set |
| bflipset | ubi-base | v | nat-set |
| bflipset-cons | ubi-base | p | nat-set × wlarray |
| bool | bool | s | |
| boolvar | bool | v | bool |
| boolvar0 | bool | v | bool |
| boolvar1 | encoding-nat | v | bool |
| buf | buffer | v | buffer |
| buf0 | buffer | v | buffer |
| buf1 | buffer | v | buffer |
| buf2 | buffer | v | buffer |
| buffer | buffer | s | |
| butlastn | erasequeue-base | pf | nat × queue → queue with λ n, q. n ≤ # q |
| butlastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| checksum | checksum | f | buffer × nat → nat |
| cmp | abstract-volume | pp | abstract-volume × leb × nat × nat with λ evol, leb, m, n. m + n ≤ # evol |
| cmp | abstract-volume | pp | abstract-volume × nat × abstract-volume × nat × nat with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0 |
| cmp | ebatbl | pp | ebatbl × ebaentry × nat × nat with λ ebatbl, ebae, m, n. m + n ≤ # ebatbl |
| cmp | ebatbl | pp | ebatbl × nat × ebatbl × nat × nat with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0 |
| cmp | wlarray-base | pp | wlarray × nat × wlarray × nat × nat with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0 |
| cmp | apebs | pp | apebs × apeb × nat × nat with λ apebs, apeb, m, n. m + n ≤ # apebs |
| cmp | wlarray-base | pp | wlarray × wlentry × nat × nat with λ wlar, wle, m, n. m + n ≤ # wlar |
| cmp | apebs | pp | apebs × nat × apebs × nat × nat with λ apebs, m, apebs0, m0, n. m + n ≤ # apebs ∧ m0 + n ≤ # apebs0 |
| 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 | wlarray-base | pf | wlarray × nat × wlarray × nat × nat → wlarray with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0 |
| copy | abstract-volume | pf | abstract-volume × nat × abstract-volume × nat × nat → abstract-volume with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0 |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | ebatbl | pf | ebatbl × nat × ebatbl × nat × nat → ebatbl with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0 |
| copy | apebs | pf | apebs × nat × apebs × nat × nat → apebs with λ apebs, m, apebs0, m0, n. m + n ≤ # apebs ∧ m0 + n ≤ # apebs0 |
| count | nat-bag | f | nat × nat-bag → nat |
| d | data | v | data |
| d0 | data | v | data |
| d1 | data | v | data |
| d2 | data | v | data |
| data | data | s | |
| datasize | datasize | f | buffer → nat |
| datasize | datasize | f | buffer × nat → nat |
| decode_nat# | encoding-nat | pr | nat × buffer : nat × nat : error (nondeterministic) |
| decode_volid# | encoding-volid | pr | nat × buffer : volid × nat : error (nondeterministic) |
| decode_vtbl# | encoding-vtbl | pr | buffer : : vtbl × error (nondeterministic) |
| disj | erasequeue-base | p | queue × queue |
| 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 |
| dups | erasequeue-base | p | queue |
| ebae | ebaentry | v | ebaentry |
| ebae0 | ebaentry | v | ebaentry |
| ebae1 | ebaentry | v | ebaentry |
| ebae2 | ebaentry | v | ebaentry |
| ebaentry | ebaentry | s | |
| ebatbl | ebatbl | s | |
| ebatbl | ebatbl | v | ebatbl |
| ebatbl0 | ebatbl | v | ebatbl |
| ebatbl1 | ebatbl | v | ebatbl |
| ebatbl2 | ebatbl | v | ebatbl |
| ebm-cons | ebm-base | p | abstract-volume |
| ebm-cons | ebm-base | p | abstract-volumes |
| ebm-initial | ebm-base | p | abstract-volumes |
| empty | aecheader | c | aecheader |
| empty | buffer | c | data |
| empty | avidheader | c | avidheader |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| encode_nat# | encoding-nat | pr | nat × nat : buffer × nat : error (nondeterministic) |
| encode_volid# | encoding-volid | pr | volid × nat : buffer × nat : error (nondeterministic) |
| encode_vtbl# | encoding-vtbl | pr | : vtbl × buffer : error (nondeterministic) |
| encoding-size | encoding-nat | f | nat → nat |
| encoding-size | encoding-volid | f | volid → nat |
| eq-entry | erasequeueentry | f | nat × lebref → erasequeueentry |
| eqent | erasequeueentry | v | erasequeueentry |
| eqent0 | erasequeueentry | v | erasequeueentry |
| eqent1 | erasequeue-base | v | erasequeueentry |
| eqent2 | erasequeue-base | v | erasequeueentry |
| erase-worker-inv | ubi-base | p | apebs × wlarray × nat × error × apebs × volumes × wlarray × queue × erasequeueentry × queue × nat-set × nat × nat |
| erased | leb | c | leb |
| erasequeueentry | erasequeueentry | s | |
| erasing | wlstatus | c | wlstatus |
| err | error | v | error |
| err0 | error | v | error |
| err1 | error | v | error |
| erroneous | wlstatus | c | wlstatus |
| error | error | s | |
| evol | abstract-volume | v | abstract-volume |
| evol0 | abstract-volume | v | abstract-volume |
| evol1 | abstract-volume | v | abstract-volume |
| evol2 | abstract-volume | v | abstract-volume |
| f | wlarray-base | v | wlentry → wlentry |
| fail# | error-class | pr | : : error (nondeterministic) |
| fail_or_success# | error-class | pr | : : error (nondeterministic) |
| fill | abstract-volume | pf | abstract-volume × leb × nat × nat → abstract-volume with λ evol, leb, n, m. n + m ≤ # evol |
| fill | ebatbl | pf | ebatbl × ebaentry × nat × nat → ebatbl with λ ebatbl, ebae, n, m. n + m ≤ # ebatbl |
| fill | wlarray-base | f | wlarray × wlentry → wlarray |
| fill | apebs | pf | apebs × apeb × nat × nat → apebs with λ apebs, apeb, n, m. n + m ≤ # apebs |
| fill | buffer | f | buffer × data → buffer |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fill | apebs | f | apebs × apeb → apebs |
| fill | wlarray-base | pf | wlarray × wlentry × nat × nat → wlarray with λ wlar, wle, n, m. n + m ≤ # wlar |
| fill | ebatbl | f | ebatbl × ebaentry → ebatbl |
| fill | abstract-volume | f | abstract-volume × leb → abstract-volume |
| fillfirst | nat-list-set | f | nat × nat × nat-list → nat-list |
| fillfirst | erasequeue-base | f | nat × erasequeueentry × queue → queue |
| filter | erasequeue-base | f | queue × queue → queue |
| firstn | erasequeue-base | pf | nat × queue → queue with λ n, q. n ≤ # q |
| firstn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| fn | array-indices | v | nat → nat |
| free | wlstatus | c | wlstatus |
| free-ecs | wlarray | f | wlarray → nat-set |
| free-ecs | wlarray | f | wlarray × nat → nat-set |
| frome | erasequeue-base | f | queue × erasequeueentry → queue |
| frome | nat-list-set | f | nat-list × nat → nat-list |
| garbage | aecheader | c | aecheader |
| garbage | avidheader | c | avidheader |
| id | ubi-base | p | apebs × apebs × nat-set |
| id○ | abstract-volume | p | abstract-volume × abstract-volume × nat |
| id○ | wlarray-base | p | wlarray × wlarray × nat |
| id○ | ebatbl | p | ebatbl × ebatbl × nat |
| id○ | buffer | p | buffer × buffer × nat |
| id○ | apebs | p | apebs × apebs × nat |
| idrange | abstract-volume | pp | abstract-volume × nat × nat with λ evol, m, n. m + n ≤ # evol |
| idrange | ebatbl | pp | ebatbl × nat × nat with λ ebatbl, m, n. m + n ≤ # ebatbl |
| idrange | apebs | pp | apebs × nat × nat with λ apebs, m, n. m + n ≤ # apebs |
| idrange | buffer | pp | buffer × nat × nat with λ buf, m, n. m + n ≤ # buf |
| idrange | wlarray-base | pp | wlarray × nat × nat with λ wlar, m, n. m + n ≤ # wlar |
| is-aligned | align | p | nat × nat |
| is-encoded | encoding-nat | p | nat × buffer |
| is-encoded | encoding-vtbl | p | vtbl × buffer |
| is-encoded | encoding-volid | p | volid × buffer |
| is-encoded-rec | encoding-vtbl | p | vtbl × buffer |
| is-garbage-nat | encoding-nat | p | buffer |
| is-garbage-volid | encoding-volid | p | buffer |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| lastn | erasequeue-base | pf | nat × queue → queue with λ n, q. n ≤ # q |
| lastn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| leb | leb | s | |
| leb | leb | v | leb |
| leb0 | abstract-volume | v | leb |
| leb1 | abstract-volume | v | leb |
| lebref | lebref | s | |
| lebrefset | lebrefset | s | |
| lref | lebref | v | lebref |
| lref0 | lebrefset | v | lebref |
| lref1 | lebrefset | v | lebref |
| m | nat-basic | v | nat |
| m0 | wlentry | v | nat |
| m1 | avidheader | v | nat |
| m2 | avidheader | v | nat |
| m3 | avidheader | v | nat |
| m4 | avidheader | v | nat |
| m5 | avidheader | v | nat |
| m6 | avidheader | v | nat |
| mapped | leb | f | buffer × nat → leb |
| mapped-pebs | ubi-base | f | volumes → nat-set |
| max | min-max | f | nat × nat → nat |
| max-avol | ubi-abs | f | apebs × ebatbl × volid × queue → abstract-volume |
| max-avols | ubi-abs | f | apebs × volumes × queue → abstract-volumes |
| min | min-max | f | nat × nat → nat |
| mkabstractvolume | abstract-volume | f | nat → abstract-volume |
| mkapebs | apebs | f | nat → apebs |
| mkbuf | buffer | f | nat → buffer |
| mkebatbl | ebatbl | f | nat → ebatbl |
| mkempbuf | buffer | f | nat → buffer |
| mklist | nat-list-set | f | nat × nat → nat-list |
| mklist | erasequeue-base | f | erasequeueentry × nat → queue |
| mkpeb | apeb | f | aecheader × avidheader × buffer × nat × bool → apeb |
| mkwlarray | wlarray-base | f | nat → wlarray |
| 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-bag | nat-bag | s | |
| nat-list | nat-list-set | s | |
| nat-set | nat-set | s | |
| none | lebref | c | lebref |
| 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 |
| pos | nat-list-set | f | nat × nat-list → nat |
| pos | erasequeue-base | f | erasequeueentry × queue → nat |
| prefixn | nat-list-set | f | nat × nat-list → nat-list |
| q | erasequeue-base | v | queue |
| q0 | erasequeue-base | v | queue |
| q1 | erasequeue-base | v | queue |
| q2 | erasequeue-base | v | queue |
| q5 | erasequeue-base | v | queue |
| queue | erasequeue-base | s | |
| range= | buffer | p | buffer × nat × buffer × nat × nat |
| resize | buffer | f | buffer × nat → buffer |
| restn | erasequeue-base | pf | nat × queue → queue with λ n, q. n ≤ # q |
| restn | nat-list-set | pf | nat × nat-list → nat-list with λ n, nx. n ≤ # nx |
| rev | abstract-volume | pf | abstract-volume × nat → abstract-volume with λ evol, n. n ≤ # evol |
| rev | ebatbl | pf | ebatbl × nat → ebatbl with λ ebatbl, n. n ≤ # ebatbl |
| rev | nat-list-set | f | nat-list → nat-list |
| rev | apebs | pf | apebs × nat → apebs with λ apebs, n. n ≤ # apebs |
| rev | wlarray-base | f | wlarray → wlarray |
| rev | buffer | pf | buffer × nat → buffer with λ buf, n. n ≤ # buf |
| rev | buffer | f | buffer → buffer |
| rev | wlarray-base | pf | wlarray × nat → wlarray with λ wlar, n. n ≤ # wlar |
| rev | apebs | f | apebs → apebs |
| rev | abstract-volume | f | abstract-volume → abstract-volume |
| rev | ebatbl | f | ebatbl → ebatbl |
| rev | erasequeue-base | f | queue → queue |
| rmdup | nat-list-set | f | nat-list → nat-list |
| rmdup | erasequeue-base | f | queue → queue |
| s | lebrefset | v | lebrefset |
| s0 | lebrefset | v | lebrefset |
| s1 | lebrefset | v | lebrefset |
| s2 | lebrefset | v | lebrefset |
| same-used | wlarray | p | wlarray × wlarray |
| slice | nat-list-set | f | nat × nat × nat-list → nat-list |
| splice | buffer | f | buffer × nat × buffer × nat × nat → buffer |
| stat | wlstatus | v | wlstatus |
| stat0 | wlentry | v | wlstatus |
| subarray | abstract-volume | pf | abstract-volume × nat × nat → abstract-volume with λ evol, m, n. m + n ≤ # evol |
| subarray | wlarray-base | pf | wlarray × nat × nat → wlarray with λ wlar, m, n. m + n ≤ # wlar |
| subarray | ebatbl | pf | ebatbl × nat × nat → ebatbl with λ ebatbl, m, n. m + n ≤ # ebatbl |
| subarray | buffer | pf | buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf |
| subarray | apebs | pf | apebs × nat × nat → apebs with λ apebs, m, n. m + n ≤ # apebs |
| sublist | erasequeue-base | pf | nat × nat × queue → queue with λ n, m, q. n + m ≤ # q |
| sublist | nat-list-set | pf | nat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx |
| to-vtbl | vtbl-conv | f | volumes → vtbl |
| ubi-cons | ubi-base | p | apebs × volumes × wlarray × queue × nat-set × nat × nat |
| ubi-io-erase-pre | ubi-io-pre | p | nat × apebs |
| ubi-io-initial | ubi-io-inv | p | apebs |
| ubi-io-inv | ubi-io-inv | p | apebs |
| ubi-io-isbad-pre | ubi-io-pre | p | nat × apebs |
| ubi-io-markbad-pre | ubi-io-pre | p | nat × apebs |
| ubi-io-peb-initial | ubi-io-inv | p | apeb |
| ubi-io-peb-inv | ubi-io-inv | p | apeb |
| ubi-io-read-data-pre | ubi-io-pre | p | nat × nat × nat × nat × buffer × apebs |
| ubi-io-read-echdr-pre | ubi-io-pre | p | nat × apebs |
| ubi-io-read-vidhdr-pre | ubi-io-pre | p | nat × apebs |
| ubi-io-write-data-pre | ubi-io-pre | p | nat × nat × nat × nat × buffer × apebs |
| ubi-io-write-data-wl-pre | ubi-io-pre | p | nat × nat × buffer × apebs |
| ubi-io-write-echdr-pre | ubi-io-pre | p | nat × aecheader × apebs |
| ubi-io-write-vidhdr-pre | ubi-io-pre | p | nat × avidheader × apebs |
| unique-elems | bag-max | p | nat-bag |
| unique-sqns | ubi-base | p | apebs |
| unmapped | ebaentry | c | ebaentry |
| unmapped | leb | c | leb |
| used | wlstatus | c | wlstatus |
| used-ecs | wlarray | f | wlarray → nat-set |
| used-ecs | wlarray | f | wlarray × nat → nat-set |
| v | volid | v | volid |
| v0 | volid | v | volid |
| v1 | volid | v | volid |
| v2 | volid | v | volid |
| valid-ebatbl | ubi-base | p | apebs × wlarray × volumes × nat |
| valid-eraseq | ubi-base | p | apebs × queue |
| valid-eraseq | ubi-base | p | queue |
| valid-eraseq | ubi-base | p | wlarray × queue |
| valid-global-sqn | ubi-base | p | apebs × nat |
| valid-indices | wlarray-base | p | wlarray × nat-list |
| valid-leb | ebm-base | p | leb |
| valid-peb | valid-peb | p | volid × nat × apeb |
| valid-peb | valid-peb | p | apeb |
| valid-sqns | sqns | f | volid × nat × apebs → nat-bag |
| valid-sqns | sqns | f | volid × nat × apebs × nat → nat-bag |
| valid-vtbl | ubi-base | p | apebs × volumes × wlarray × nat |
| valid-wl | ubi-base | p | apebs × wlarray |
| valid-wl-entry | ubi-base | p | apeb × wlentry |
| volid | volid | s | |
| vols | volumes | v | volumes |
| vols0 | volumes | v | volumes |
| vols1 | volumes | v | volumes |
| vols2 | volumes | v | volumes |
| volumes | volumes | s | |
| vtbl | vtbl | s | |
| vtbl | vtbl | v | vtbl |
| vtbl0 | vtbl | v | vtbl |
| vtbl1 | vtbl | v | vtbl |
| vtbl2 | vtbl | v | vtbl |
| wl-entry | wlentry | f | nat × wlstatus → wlentry |
| wlar | wlarray-base | v | wlarray |
| wlar0 | wlarray-base | v | wlarray |
| wlar1 | wlarray-base | v | wlarray |
| wlar2 | wlarray-base | v | wlarray |
| wlarray | wlarray-base | s | |
| wle | wlentry | v | wlentry |
| wle0 | wlarray-base | v | wlentry |
| wle1 | wlarray-base | v | wlentry |
| wlentry | wlentry | s | |
| wlstatus | wlstatus | s | |
| write-once-inv | ubi-base | p | apebs × volumes × wlarray × queue × nat-set × nat × nat × volid × nat × nat × nat × buffer × error |
| zero | buffer | c | data |