| Symbol | Specification | Kind | Type |
|---|
| # . | nat-list-set | f | nat-list → nat |
| # . | string | f | string → nat |
| # . | nat-set | f | nat-set → nat |
| # . | recovery-entries | f | recoveryentries → 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 |
| . ' | string | f | char → string |
| . ' | nat-list-set | f | nat → nat-list |
| . ' | erasequeue-base | f | erasequeueentry → queue |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | nat-list-set | f | nat × nat-list → nat-list |
| . + . | string | f | string × char → string |
| . + . | nat-list-set | f | nat-list × nat-list → nat-list |
| . + . | string | f | string × string → string |
| . + . | nat-list-set | f | nat-list × nat → nat-list |
| . + . | string | f | char × string → string |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | erasequeue-base | f | queue × erasequeueentry → queue |
| . + . | erasequeue-base | f | erasequeueentry × queue → queue |
| . + . | erasequeue-base | f | queue × queue → queue |
| . ++ . | string | f | string × char → string |
| . ++ . | nat-list-set | f | nat-list × nat → nat-list |
| . ++ . | lebrefset | f | lebrefset × lebref → lebrefset |
| . ++ . | nat-set | f | nat-set × nat → nat-set |
| . ++ . | erasequeue-base | f | queue × erasequeueentry → queue |
| . ++ . | 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 |
| . +2 . | string | f | char × char → string |
| . - . | 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 |
| . -- . | recovery-entries | f | recoveryentries × lebadress → recoveryentries |
| . -- . | 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 . | string | f | string × char → string |
| . -1l . | erasequeue-base | f | queue × erasequeueentry → queue |
| . -l . | nat-list-set | f | nat-list × nat → nat-list |
| . -l . | string | f | string × char → string |
| . -l . | erasequeue-base | f | queue × erasequeueentry → queue |
| . -p . | nat-list-set | f | nat-list × nat → nat-list |
| . -p . | string | f | string × nat → string |
| . -p . | erasequeue-base | f | queue × nat → queue |
| . .bad | apeb | p | apeb |
| . .bad:= . | apeb | f | apeb × bool → apeb |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .butlast | nat-list-set | pf | nat-list → nat-list with λ nx. nx ≠ [] |
| . .butlast | erasequeue-base | pf | queue → queue with λ q. q ≠ [] |
| . .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 ≠ "" |
| . .checksum | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .checksum:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .data | apeb | f | apeb → buffer |
| . .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 | apeb | f | apeb → nat |
| . .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 | string | pf | string → char with λ str. str ≠ "" |
| . .last | erasequeue-base | pf | queue → erasequeueentry with λ q. q ≠ [] |
| . .last | nat-list-set | pf | nat-list → nat with λ nx. nx ≠ [] |
| . .leb | lebadress | f | lebadress → nat |
| . .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? |
| . .leb:= . | lebadress | f | lebadress × nat → lebadress |
| . .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 |
| . .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 | recovery-entry | f | recoveryentry → nat |
| . .pnum:= . | ebaentry | pf | ebaentry × nat → ebaentry with λ ebae, m. ebae ≠ unmapped |
| . .pnum:= . | erasequeueentry | f | erasequeueentry × nat → erasequeueentry |
| . .pnum:= . | recovery-entry | f | recoveryentry × nat → recoveryentry |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .size | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .size:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .sqn | recovery-entry | f | recoveryentry → nat |
| . .sqn | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .sqn:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .sqn:= . | recovery-entry | f | recoveryentry × nat → recoveryentry |
| . .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 |
| . .toString | debug | f | nat → string |
| . .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 | lebadress | f | lebadress → volid |
| . .vol | avidheader | pf | avidheader → volid with λ avhdr. avhdr.valid? |
| . .vol:= . | lebref | pf | lebref × volid → lebref with λ lref, v. lref ≠ none |
| . .vol:= . | lebadress | f | lebadress × volid → lebadress |
| . .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 |
| . [ . ] | string | pf | string × nat × char → string with λ str, n, char. n < # str |
| . [ . ] | string | pf | string × nat → char with λ str, n. n < # str |
| . [ . ] | recovery-entries | pf | recoveryentries × lebadress → recoveryentry with λ recs, ladr. ladr ∈ recs |
| . [ . ] | erasequeue-base | pf | queue × nat × erasequeueentry → queue with λ q, n, eqent. n < # q |
| . [ . ] | erasequeue-base | pf | queue × nat → erasequeueentry with λ q, n. n < # q |
| . [ . ] | vtbl | f | vtbl × volid × nat → vtbl |
| . [ . ] | volumes | pf | volumes × volid → ebatbl with λ vols, v. v ∈ vols |
| . [ . ] | volumes | f | volumes × volid × ebatbl → volumes |
| . [ . ] | ebatbl | pf | ebatbl × nat × ebaentry → ebatbl with λ ebatbl, n, ebae. n < # ebatbl |
| . [ . ] | recovery-entries | f | recoveryentries × lebadress × recoveryentry → recoveryentries |
| . [ . ] | ebatbl | pf | ebatbl × nat → ebaentry with λ ebatbl, n. n < # ebatbl |
| . [ . ] | nat-list-set | pf | nat-list × nat → nat with λ nx, n. n < # nx |
| . [ . ] | vtbl | pf | vtbl × volid → nat with λ vtbl, v. v ∈ vtbl |
| . [ . ] | nat-list-set | pf | nat-list × nat × nat → nat-list with λ nx, n, n0. n < # nx |
| . [ . ] | apebs | pf | apebs × nat × apeb → apebs with λ apebs, n, apeb. n < # apebs |
| . [ . ] | wlarray-base | pf | wlarray × nat → wlentry with λ wlar, n. n < # wlar |
| . [ . ] | apebs | pf | apebs × nat → apeb with λ apebs, n. n < # apebs |
| . [ . ] | wlarray-base | pf | wlarray × nat × wlentry → wlarray with λ wlar, n, wle. n < # wlar |
| . [ . ] | 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 |
| . \ . | nat-bag | f | nat-bag × nat-bag → nat-bag |
| . \ . | erasequeue-base | f | queue × queue → queue |
| . \ . | lebrefset | f | lebrefset × lebrefset → lebrefset |
| . × . | lebadress | f | volid × nat → lebadress |
| . × . | lebref | f | volid × nat → lebref |
| . ∈ . | string | p | char × string |
| . ∈ . | nat-list-set | p | nat × nat-list |
| . ∈ . | recovery-entries | p | lebadress × recoveryentries |
| . ∈ . | 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 |
| . ⊆ . | ubi-crash-recovery-base | p | volumes × volumes |
| . ⊆ . | nat-set | p | nat-set × nat-set |
| . ⊆ . | lebrefset | p | lebrefset × lebrefset |
| . ⊆ . | nat-bag | p | nat-bag × nat-bag |
| . ⊆ . | erasequeue-base | p | queue × queue |
| . ⊆ . | vtbl | p | vtbl × vtbl |
| . ⊑ . | string | p | string × string |
| . ⊑ . | nat-list-set | p | nat-list × nat-list |
| . ⊑ . | erasequeue-base | p | queue × queue |
| . ⊒ . | string | p | string × string |
| . ⊒ . | nat-list-set | p | nat-list × nat-list |
| . ⊒ . | erasequeue-base | p | queue × queue |
| . ⊥ . | ubi-crash-recovery-base | p | recoveryentries × volumes |
| . ⊥ . | vtbl | p | vtbl × vtbl |
| . ⌈ . ⌉ | ubi-crash-recovery-base | p | volumes × volumes × queue |
| . subseteq . | volumes | p | volumes × volumes |
| . subseteq . | recovery-entries | p | recoveryentries × recoveryentries |
| [] | nat-list-set | c | nat-list |
| [] | erasequeue-base | c | queue |
| { . } | nat-set | f | nat → nat-set |
| { . } | lebrefset | f | lebref → lebrefset |
| { . } | nat-bag | f | nat → nat-bag |
| Δ . | ubi-quality-base | f | wlarray → nat |
| φ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 |
| ∅ | volumes | c | volumes |
| ∅ | recovery-entries | c | recoveryentries |
| ∅ | lebrefset | c | lebrefset |
| ⊏ | string | p | string × string |
| ⌊ . ⌋ | error-class | p | error |
| ⌜ . ⌝ | ebaentry | f | nat → ebaentry |
| AEHDR | aubi-io-asm | v | aecheader,flexible |
| APEB | aubi-io-asm | v | apeb,flexible |
| APEBS | aubi-io-asm | v | apebs,flexible |
| APEBS0 | aubi-io-asm | v | apebs,flexible |
| AVHDR | aubi-io-asm | v | avidheader,flexible |
| BFLIPSET | ubi-asm | v | nat-set,flexible |
| BITFLIPS | aubi-io-asm | v | bool,flexible |
| BITFLIPS0 | ubi-asm | v | bool,flexible |
| BUF | aubi-io-asm | v | buffer,flexible |
| BUF0 | aubi-io-asm | v | buffer,flexible |
| Boolvar | encoding-nat | v | bool,flexible |
| CHKSM | ubi-asm | v | nat,flexible |
| EACCESS | error | c | error |
| EB_PAGE_SIZE | eraseblock | c | nat |
| EBADFD | error | c | error |
| EBAENT | ubi-asm | v | ebaentry,flexible |
| EBATBL | ubi-asm | v | ebatbl,flexible |
| EC | ubi-asm | v | nat,flexible |
| 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 |
| EQENT | ubi-asm | v | erasequeueentry,flexible |
| ERASEQ | ubi-asm | v | queue,flexible |
| EROFS | error | c | error |
| ERR | error-class | v | error,flexible |
| ERR0 | error-class | v | error,flexible |
| ESUCCESS | error | c | error |
| EUCLEAN | error | c | error |
| FOUND | ubi-asm | v | bool,flexible |
| FREEECS | ubi-asm | v | nat-set,flexible |
| FROM | ubi-asm | v | nat,flexible |
| INDEX | encoding-vtbl | v | nat,flexible |
| INVALIDECS | ubi-asm | v | nat-list,flexible |
| ISBAD | aubi-io-asm | v | bool,flexible |
| LADR | ubi-asm | v | lebadress,flexible |
| LEB_SIZE | eraseblock | c | nat |
| LEBSIZE | ubi-asm | v | nat,flexible |
| LNUM | ubi-asm | v | nat,flexible |
| LREF | ubi-asm | v | lebref,flexible |
| M | encoding-vtbl | v | nat,flexible |
| N | aubi-io-asm | v | nat,flexible |
| N0 | aubi-io-asm | v | nat,flexible |
| N1 | aubi-io-asm | v | nat,flexible |
| OFFSET | aubi-io-asm | v | nat,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PAGESIZE | ubi-asm | v | nat,flexible |
| PEB_SIZE | eraseblock | c | nat |
| PNUM | aubi-io-asm | v | nat,flexible |
| PNUM0 | ubi-asm | v | nat,flexible |
| RECS | ubi-asm | v | recoveryentries,flexible |
| SIZE | encoding-vtbl | v | nat,flexible |
| SQNUM | ubi-asm | v | nat,flexible |
| TMPERASEQ | ubi-asm | v | queue,flexible |
| TO | ubi-asm | v | nat,flexible |
| TRIES | ubi-asm | v | nat,flexible |
| UBI_ERASE_RETRIES | ubi-base | c | nat |
| UBI_WRITE_RETRIES | ubi-base | c | nat |
| USEDECS | ubi-asm | v | nat-set,flexible |
| VALID | ubi-asm | v | bool,flexible |
| VALIDCOUNT | ubi-asm | v | nat,flexible |
| VALIDECSUM | ubi-asm | v | nat,flexible |
| VOLID | encoding-vtbl | v | volid,flexible |
| VOLID0 | ubi-asm | v | volid,flexible |
| VOLS | ubi-asm | v | volumes,flexible |
| VTBL | encoding-vtbl | v | vtbl,flexible |
| VTBL_LNUM | vtbl-conv | c | nat |
| VTBL_VOLID | vtbl-conv | c | volid |
| VTBLPNUM | ubi-asm | v | nat,flexible |
| WL_THRESHOLD | ubi-base | c | nat |
| WLARRAY | ubi-asm | v | wlarray,flexible |
| WLFREE | ubi-asm | v | wlentry,flexible |
| WLUSED | ubi-asm | v | wlentry,flexible |
| 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 |
| aubi_io_format# | aubi-io-asm | pr | : : apebs × error (nondeterministic) |
| aubi_io_get_blockcount# | aubi-io-asm | pr | apebs : : nat |
| aubi_io_get_leb_size# | aubi-io-asm | pr | apebs : : nat |
| aubi_io_get_page_size# | aubi-io-asm | pr | apebs : : nat |
| aubi_io_isbad# | aubi-io-asm | pr | nat × apebs : : bool × error (nondeterministic) |
| aubi_io_markbad# | aubi-io-asm | pr | nat : apebs : error (nondeterministic) |
| aubi_io_read_data# | aubi-io-asm | pr | nat × nat × nat × nat × apebs : buffer : bool × error (nondeterministic) |
| aubi_io_read_echdr# | aubi-io-asm | pr | nat × apebs : aecheader : bool × error (nondeterministic) |
| aubi_io_read_vidhdr# | aubi-io-asm | pr | nat × apebs : avidheader : bool × error (nondeterministic) |
| aubi_io_recovery# | aubi-io-asm | pr | apebs : (nonfunctional) |
| aubi_io_sync_erase# | aubi-io-asm | pr | nat : apebs : error (nondeterministic) |
| aubi_io_write_data# | aubi-io-asm | pr | nat × nat × nat × nat × buffer : apebs : error (nondeterministic) |
| aubi_io_write_data_wl# | aubi-io-asm | pr | nat × nat × buffer : apebs : error (nondeterministic) |
| aubi_io_write_echdr# | aubi-io-asm | pr | nat × aecheader : apebs : error (nondeterministic) |
| aubi_io_write_vidhdr# | aubi-io-asm | pr | nat × avidheader : apebs : error (nondeterministic) |
| avhdr | avidheader | v | avidheader |
| avhdr0 | avidheader | v | avidheader |
| avhdr1 | avidheader | v | avidheader |
| avidhdr | avidheader | f | volid × nat × nat × nat × nat → avidheader |
| avidheader | avidheader | s | |
| 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 |
| bitflips | aubi-io-asm | v | bool |
| 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 | string | pf | nat × string → string with λ n, str. n ≤ # str |
| 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 |
| char | char | s | |
| char | char | v | char |
| char0 | char | v | char |
| char1 | char | v | char |
| char2 | char | v | char |
| checksum | checksum | f | buffer × nat → nat |
| 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 | apebs | pp | apebs × apeb × nat × nat with λ apebs, apeb, m, n. m + n ≤ # apebs |
| cmp | apebs | pp | apebs × nat × apebs × nat × nat with λ apebs, m, apebs0, m0, n. m + n ≤ # apebs ∧ m0 + n ≤ # apebs0 |
| cmp | wlarray-base | pp | wlarray × nat × wlarray × nat × nat with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0 |
| cmp | buffer | pp | buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf |
| cmp | wlarray-base | pp | wlarray × wlentry × nat × nat with λ wlar, wle, m, n. m + n ≤ # wlar |
| cmp | buffer | pp | buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | wlarray-base | pf | wlarray × nat × wlarray × nat × nat → wlarray with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0 |
| copy | ebatbl | pf | ebatbl × nat × ebatbl × nat × nat → ebatbl with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0 |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| 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 |
| debug# | debug | pr | string : |
| 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 | string | p | string × string |
| disj | nat-list-set | p | nat-list × nat-list |
| disj | erasequeue-base | p | queue × queue |
| dropn | nat-list-set | f | nat × nat-list → nat-list |
| dups | nat-list-set | p | nat-list |
| dups | erasequeue-base | p | queue |
| dups | string | p | string |
| 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 |
| ecs | ubi-quality-base | f | wlarray → nat-bag |
| ecs | ubi-quality-base | f | wlarray × nat → nat-bag |
| 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 |
| 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 | |
| f | wlarray-base | v | wlentry → wlentry |
| fail# | error-class | pr | : : error (nondeterministic) |
| fail_or_success# | error-class | pr | : : error (nondeterministic) |
| fill | ebatbl | pf | ebatbl × ebaentry × nat × nat → ebatbl with λ ebatbl, ebae, n, m. n + m ≤ # ebatbl |
| fill | apebs | pf | apebs × apeb × nat × nat → apebs with λ apebs, apeb, n, m. n + m ≤ # apebs |
| fill | wlarray-base | f | wlarray × wlentry → wlarray |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fill | buffer | f | buffer × data → buffer |
| fill | wlarray-base | pf | wlarray × wlentry × nat × nat → wlarray with λ wlar, wle, n, m. n + m ≤ # wlar |
| fill | apebs | f | apebs × apeb → apebs |
| fill | ebatbl | f | ebatbl × ebaentry → ebatbl |
| fillfirst | nat-list-set | f | nat × nat × nat-list → nat-list |
| fillfirst | string | f | nat × char × string → string |
| fillfirst | erasequeue-base | f | nat × erasequeueentry × queue → queue |
| filter | erasequeue-base | f | queue × queue → queue |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| 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 | string | f | string × char → string |
| frome | nat-list-set | f | nat-list × nat → nat-list |
| frome | erasequeue-base | f | queue × erasequeueentry → queue |
| garbage | aecheader | c | aecheader |
| garbage | avidheader | c | avidheader |
| id | ubi-base | p | apebs × apebs × nat-set |
| 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 | 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 |
| indices-erasing | ubi-crash-recovery-base | p | wlarray × nat-list |
| is-aligned | align | p | nat × nat |
| is-encoded | encoding-nat | p | nat × buffer |
| is-encoded | encoding-volid | p | volid × buffer |
| is-encoded | encoding-vtbl | p | vtbl × buffer |
| is-encoded-rec | encoding-vtbl | p | vtbl × buffer |
| is-garbage-nat | encoding-nat | p | buffer |
| is-garbage-volid | encoding-volid | p | buffer |
| is-max | ubi-crash-recovery-base | p | apebs × volumes × wlarray × queue × nat-set × nat × nat |
| isbad | aubi-io-asm | v | bool |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| ladr | lebadress | v | lebadress |
| ladr1 | recovery-entries | v | lebadress |
| ladr2 | recovery-entries | v | lebadress |
| 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 |
| lastn | erasequeue-base | pf | nat × queue → queue with λ n, q. n ≤ # q |
| lebadress | lebadress | s | |
| 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-pebs | ubi-base | f | volumes → nat-set |
| max | min-max | f | nat × nat → nat |
| min | min-max | f | nat × nat → nat |
| 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 | string | f | char × nat → string |
| 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 | string | f | char × string → 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 |
| rec | recovery-entry | v | recoveryentry |
| rec0 | recovery-entries | v | recoveryentry |
| rec1 | recovery-entries | v | recoveryentry |
| rec2 | recovery-entries | v | recoveryentry |
| recovery-entry | recovery-entry | f | nat × nat → recoveryentry |
| recoveryentries | recovery-entries | s | |
| recoveryentry | recovery-entry | s | |
| recs | recovery-entries | v | recoveryentries |
| recs0 | recovery-entries | v | recoveryentries |
| recs1 | recovery-entries | v | recoveryentries |
| recs2 | recovery-entries | v | recoveryentries |
| resize | buffer | f | buffer × nat → buffer |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| 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 | 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 | string | f | string → string |
| 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 |
| rmdup | string | f | string → string |
| s | lebrefset | v | lebrefset |
| s0 | lebrefset | v | lebrefset |
| s1 | lebrefset | v | lebrefset |
| s2 | lebrefset | v | lebrefset |
| same-used | wlarray | p | wlarray × wlarray |
| scan-all-inv | ubi-crash-recovery-base | p | nat × apebs × recoveryentries × wlarray × queue × nat-set × nat-list × nat × error |
| slice | nat-list-set | f | nat × nat × nat-list → nat-list |
| splice | buffer | f | buffer × nat × buffer × nat × nat → buffer |
| sqnum | ubi-asm | v | nat |
| stat | wlstatus | v | wlstatus |
| stat0 | wlentry | v | wlstatus |
| str | string | v | string |
| str0 | string | v | string |
| str1 | string | v | string |
| str2 | string | v | string |
| str3 | string | v | string |
| string | string | s | |
| subarray | ebatbl | pf | ebatbl × nat × nat → ebatbl with λ ebatbl, m, n. m + n ≤ # ebatbl |
| subarray | wlarray-base | pf | wlarray × nat × nat → wlarray with λ wlar, m, n. m + n ≤ # wlar |
| subarray | apebs | pf | apebs × nat × nat → apebs with λ apebs, m, n. m + n ≤ # apebs |
| subarray | buffer | pf | buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf |
| sublist | string | pf | nat × nat × string → string with λ n, m, str. n + m ≤ # str |
| 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 |
| sum-of-differences | ubi-quality-base | f | nat × nat-bag → nat |
| 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 |
| ubi_atomic_leb_change# | ubi-asm | pr | volid × nat × nat × nat × buffer × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_change# | ubi-asm | pr | volid × nat × nat × buffer × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_create_volume# | ubi-asm | pr | volid × nat × nat × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_erase# | ubi-asm | pr | volid × nat × nat × nat
: volumes × wlarray × queue × nat-set × apebs
: error (nondeterministic) |
| ubi_erase_all# | ubi-asm | pr | volumes × nat-set × nat × nat : wlarray × queue × apebs : error (nondeterministic) |
| ubi_erase_worker# | ubi-asm | pr | : wlarray × queue × apebs (nondeterministic nonfunctional) |
| ubi_erase_worker_helper# | ubi-asm | pr | nat : wlarray × apebs : error (nondeterministic) |
| ubi_fix_ecs# | ubi-asm | pr | nat : nat-list × wlarray (nonfunctional) |
| ubi_format# | ubi-asm | pr | : wlarray × nat × nat × apebs × volumes × queue × nat-set × nat
: nat × error (nondeterministic) |
| ubi_get_leb_size# | ubi-asm | pr | nat : : nat |
| ubi_get_page_size# | ubi-asm | pr | nat : : nat |
| ubi_get_pebs_for_wl# | ubi-asm | pr | wlarray : nat × nat × nat-set : bool (nondeterministic) |
| ubi_get_volume_size# | ubi-asm | pr | volid × volumes : : nat |
| ubi_init_vols_mappings# | ubi-asm | pr | nat × apebs : recoveryentries × volumes × wlarray × queue × nat-set (nondeterministic nonfunctional) |
| ubi_init_vols_sizes# | ubi-asm | pr | recoveryentries × wlarray × apebs : vtbl × volumes (nondeterministic nonfunctional) |
| ubi_map# | ubi-asm | pr | volid × nat × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_next_sqnum# | ubi-asm | pr | : nat : nat |
| ubi_read# | ubi-asm | pr | volid × nat × nat × nat × nat × volumes × nat × apebs
: buffer × nat-set
: error (nondeterministic) |
| ubi_recover# | ubi-asm | pr | apebs
: volumes × wlarray × queue × nat-set × nat × nat × nat
: nat × error (nondeterministic) |
| ubi_scan_all# | ubi-asm | pr | nat × apebs
: recoveryentries × wlarray × queue × nat-set × nat
: nat × nat × nat-list × error (nondeterministic) |
| ubi_sync_device# | ubi-asm | pr | volumes × nat-set × nat × nat : wlarray × queue × apebs : error (nondeterministic) |
| ubi_unmap# | ubi-asm | pr | volid × nat : volumes × wlarray × queue × nat-set (nonfunctional) |
| ubi_wear_leveling_worker# | ubi-asm | pr | nat × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_wl_find_free_max_below# | ubi-asm | pr | nat × wlarray : nat (nonfunctional) |
| ubi_wl_get_free_min# | ubi-asm | pr | wlarray : nat : bool |
| ubi_wl_get_peb# | ubi-asm | pr | : nat × wlarray × queue × apebs : error (nondeterministic) |
| ubi_wl_get_used_min# | ubi-asm | pr | wlarray : nat : bool |
| ubi_wl_put_peb# | ubi-asm | pr | lebref × nat : wlarray × queue (nonfunctional) |
| ubi_write# | ubi-asm | pr | volid × nat × nat × nat × nat × buffer × nat
: volumes × wlarray × queue × nat-set × nat × nat × apebs
: error (nondeterministic) |
| ubi_write_multiple# | ubi-asm | pr | volid × nat × nat × nat × nat × buffer × nat-set × nat
: volumes × wlarray × queue × nat × apebs
: error (nondeterministic) |
| ubi_write_once# | ubi-asm | pr | volid × nat × nat × nat × nat × buffer
: volumes × wlarray × queue × nat × apebs
: error (nondeterministic) |
| unique-elems | bag-max | p | nat-bag |
| unique-sqns | ubi-base | p | apebs |
| unmapped | ebaentry | c | ebaentry |
| unmapped-vols | ubi-crash-recovery-base | p | volumes |
| 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 | queue |
| valid-eraseq | ubi-base | p | apebs × queue |
| valid-eraseq | ubi-base | p | wlarray × queue |
| valid-eraseq-strong | ubi-crash-recovery-base | p | apebs × vtbl × queue |
| valid-eraseq-stronger | ubi-crash-recovery-base | p | apebs × queue |
| valid-global-sqn | ubi-base | p | apebs × nat |
| valid-indices | wlarray-base | p | wlarray × nat-list |
| valid-peb | valid-peb | p | volid × nat × apeb |
| valid-peb | valid-peb | p | apeb |
| valid-recs | ubi-crash-recovery-base | p | apebs × wlarray × recoveryentries |
| valid-recs-sqns | ubi-crash-recovery-base | p | apebs × recoveryentries |
| 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-vtbl-weak | ubi-crash-recovery-base | p | apebs × 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 |
| vtblpnum | ubi-asm | v | nat |
| 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 |