| Symbol | Specification | Kind | Type |
|---|
| # . | buffer | f | buffer → nat |
| # . | string | f | string → nat |
| # . | pebs | f | pebs → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . ' | string | f | char → string |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . + . | buffer | f | buffer × buffer → buffer |
| . + . | string | f | string × char → string |
| . + . | string | f | char × string → string |
| . + . | string | f | string × string → string |
| . ++ . | string | f | string × char → string |
| . +1 | nat-basic | f | nat → nat |
| . +2 . | string | f | char × char → string |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . -1l . | string | f | string × char → string |
| . -l . | string | f | string × char → string |
| . -p . | string | f | string × nat → string |
| . .bad | peb | p | peb |
| . .bad:= . | peb | f | peb × bool → peb |
| . .butlast | string | pf | string → string with λ str. str ≠ "" |
| . .char1 | string | pf | string → char with λ str. str ≠ "" |
| . .checksum | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .checksum | vidheader | f | vidheader → nat |
| . .checksum:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .checksum:= . | vidheader | f | vidheader × nat → vidheader |
| . .data | peb | f | peb → buffer |
| . .data:= . | peb | f | peb × buffer → peb |
| . .ec | aecheader | pf | aecheader → nat with λ aehdr. aehdr.valid? |
| . .ec | echeader | f | echeader → nat |
| . .ec:= . | aecheader | pf | aecheader × nat → aecheader with λ aehdr, m. aehdr.valid? |
| . .ec:= . | echeader | f | echeader × nat → echeader |
| . .fill | peb | f | peb → nat |
| . .fill:= . | peb | f | peb × nat → peb |
| . .last | string | pf | string → char with λ str. str ≠ "" |
| . .leb | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .leb | vidheader | f | vidheader → nat |
| . .leb:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .leb:= . | vidheader | f | vidheader × nat → vidheader |
| . .rstring | string | pf | string → string with λ str. str ≠ "" |
| . .size | vidheader | f | vidheader → nat |
| . .size | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .size:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .size:= . | vidheader | f | vidheader × nat → vidheader |
| . .sqn | vidheader | f | vidheader → nat |
| . .sqn | avidheader | pf | avidheader → nat with λ avhdr. avhdr.valid? |
| . .sqn:= . | avidheader | pf | avidheader × nat → avidheader with λ avhdr, m. avhdr.valid? |
| . .sqn:= . | vidheader | f | vidheader × nat → vidheader |
| . .toString | debug | f | nat → string |
| . .valid? | aecheader | p | aecheader |
| . .valid? | avidheader | p | avidheader |
| . .vol | avidheader | pf | avidheader → volid with λ avhdr. avhdr.valid? |
| . .vol | vidheader | f | vidheader → volid |
| . .vol:= . | avidheader | pf | avidheader × volid → avidheader with λ avhdr, v. avhdr.valid? |
| . .vol:= . | vidheader | f | vidheader × volid → vidheader |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × 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 |
| . [ . ] | pebs | pf | pebs × nat × peb → pebs with λ pebs, n, peb. n < # pebs |
| . [ . ] | pebs | pf | pebs × nat → peb with λ pebs, n. n < # pebs |
| . [ . ] | buffer | pf | buffer × nat → data with λ buf, n. n < # buf |
| . [ . ] | buffer | pf | buffer × nat × data → buffer with λ buf, n, d. n < # buf |
| . ∈ . | buffer | p | data × buffer |
| . ∈ . | string | p | char × string |
| . ∈ . | pebs | p | peb × pebs |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊑ . | string | p | string × string |
| . ⊒ . | string | p | string × string |
| ⊏ | string | p | string × string |
| ⌊ . ⌋ | error-class | p | error |
| AEHDR | ubi-io-asm | v | aecheader,flexible |
| AVHDR | ubi-io-asm | v | avidheader,flexible |
| BITFLIPS | mtd-asm | v | bool,flexible |
| BUF | mtd-asm | v | buffer,flexible |
| BUF0 | mtd-asm | v | buffer,flexible |
| Boolvar | encoding-echeader | 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 |
| EHDR | ubi-io-asm | v | echeader,flexible |
| EINVAL | error | c | error |
| EIO | error | c | error |
| EISDIR | error | c | error |
| ENCODED_EC_HEADER_SIZE | encoding-echeader | c | nat |
| ENCODED_VIDHEADER_SIZE | encoding-vidheader | 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 |
| ISBAD | mtd-asm | v | bool,flexible |
| LEB_SIZE | eraseblock | c | nat |
| M | ubi-io-asm | v | nat,flexible |
| N | mtd-asm | v | nat,flexible |
| N0 | mtd-asm | v | nat,flexible |
| N1 | mtd-asm | v | nat,flexible |
| OFFSET | mtd-asm | v | nat,flexible |
| PAGES_PER_LEB | eraseblock | c | nat |
| PAGES_PER_PEB | eraseblock | c | nat |
| PAGESIZE | ubi-io-asm | v | nat,flexible |
| PEB | mtd-asm | v | peb,flexible |
| PEB_SIZE | eraseblock | c | nat |
| PEBS | mtd-asm | v | pebs,flexible |
| PNUM | mtd-asm | v | nat,flexible |
| PNUM0 | mtd-asm | v | nat,flexible |
| TRIES | ubi-io-asm | v | nat,flexible |
| UBI_READ_RETRIES | ubi-io-asm | c | nat |
| VHDR | ubi-io-asm | v | vidheader,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 |
| avhdr | avidheader | v | avidheader |
| avhdr0 | avidheader | v | avidheader |
| avhdr1 | avidheader | v | avidheader |
| avidhdr | avidheader | f | volid × nat × nat × nat × nat → avidheader |
| avidheader | avidheader | s | |
| bitflips | mtd-asm | v | bool |
| bool | bool | s | |
| boolvar | bool | v | bool |
| boolvar0 | bool | v | bool |
| boolvar1 | encoding-echeader | 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 |
| 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 | pebs | pp | pebs × peb × nat × nat with λ pebs, peb, m, n. m + n ≤ # pebs |
| cmp | pebs | pp | pebs × nat × pebs × nat × nat with λ pebs, m, pebs0, m0, n. m + n ≤ # pebs ∧ m0 + n ≤ # pebs0 |
| cmp | buffer | pp | buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf |
| cmp | buffer | pp | buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | buffer | pf | buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0 |
| copy | pebs | pf | pebs × nat × pebs × nat × nat → pebs with λ pebs, m, pebs0, m0, n. m + n ≤ # pebs ∧ m0 + n ≤ # pebs0 |
| d | data | v | data |
| d0 | data | v | data |
| d1 | data | v | data |
| d2 | data | v | data |
| data | data | s | |
| debug# | debug | pr | string : |
| decode_echeader# | encoding-echeader | pr | nat × buffer : echeader : error (nondeterministic) |
| decode_echeader_empty# | encoding-echeader | pr | nat × buffer : echeader × nat : error (nondeterministic) |
| decode_echeader_nonempty# | encoding-echeader | pr | nat × buffer : echeader : error (nondeterministic) |
| decode_vidheader# | encoding-vidheader | pr | nat × buffer : vidheader : error (nondeterministic) |
| decode_vidheader_empty# | encoding-vidheader | pr | nat × buffer : vidheader × nat : error (nondeterministic) |
| decode_vidheader_nonempty# | encoding-vidheader | pr | nat × buffer : vidheader : error (nondeterministic) |
| disj | string | p | string × string |
| dups | string | p | string |
| echdr | echeader | f | nat → echeader |
| echeader | echeader | s | |
| ehdr | echeader | v | echeader |
| ehdr0 | encoding-echeader | v | echeader |
| ehdr1 | encoding-echeader | v | echeader |
| empty | buffer | c | data |
| empty | avidheader | c | avidheader |
| empty | aecheader | c | aecheader |
| emptyleb | eraseblock | c | buffer |
| emptypage | eraseblock | c | buffer |
| emptypeb | eraseblock | c | buffer |
| encode_echeader# | encoding-echeader | pr | nat × echeader : buffer : error (nondeterministic) |
| encode_echeader_empty# | encoding-echeader | pr | echeader × nat : buffer × nat : error (nondeterministic) |
| encode_echeader_nonempty# | encoding-echeader | pr | echeader × nat : buffer : error (nondeterministic) |
| encode_vidheader# | encoding-vidheader | pr | nat × vidheader : buffer : error (nondeterministic) |
| encode_vidheader_empty# | encoding-vidheader | pr | vidheader × nat : buffer × nat : error (nondeterministic) |
| encode_vidheader_nonempty# | encoding-vidheader | pr | vidheader × nat : buffer : error (nondeterministic) |
| encoding-size | encoding-echeader | f | echeader → nat |
| encoding-size | encoding-vidheader | f | vidheader → nat |
| err | error | v | error |
| err0 | error | v | error |
| err1 | error | v | error |
| error | error | s | |
| fail# | error-class | pr | : : error (nondeterministic) |
| fail_or_success# | error-class | pr | : : error (nondeterministic) |
| fill | buffer | f | buffer × data → buffer |
| fill | pebs | pf | pebs × peb × nat × nat → pebs with λ pebs, peb, n, m. n + m ≤ # pebs |
| fill | pebs | f | pebs × peb → pebs |
| fill | buffer | pf | buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf |
| fillfirst | string | f | nat × char × string → string |
| firstn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| frome | string | f | string × char → string |
| garbage | aecheader | c | aecheader |
| garbage | avidheader | c | avidheader |
| id○ | pebs | p | pebs × pebs × nat |
| id○ | buffer | p | buffer × buffer × nat |
| idrange | pebs | pp | pebs × nat × nat with λ pebs, m, n. m + n ≤ # pebs |
| idrange | buffer | pp | buffer × nat × nat with λ buf, m, n. m + n ≤ # buf |
| is-aligned | align | p | nat × nat |
| is-encoded | encoding-vidheader | p | vidheader × buffer |
| is-encoded | encoding-echeader | p | echeader × buffer |
| is-encoded-empty | encoding-echeader | p | echeader × buffer |
| is-encoded-empty | encoding-vidheader | p | vidheader × buffer |
| is-encoded-nonempty | encoding-vidheader | p | vidheader × buffer |
| is-encoded-nonempty | encoding-echeader | p | echeader × buffer |
| is-garbage-ec | encoding-echeader | p | buffer |
| is-garbage-empty-ec | encoding-echeader | p | buffer |
| is-garbage-empty-vid | encoding-vidheader | p | buffer |
| is-garbage-nonempty-ec | encoding-echeader | p | buffer |
| is-garbage-nonempty-vid | encoding-vidheader | p | buffer |
| is-garbage-vid | encoding-vidheader | p | buffer |
| isbad | mtd-asm | v | bool |
| isempty | eraseblock | p | buffer |
| isempty | eraseblock | p | buffer × nat × nat |
| lastn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| m | nat-basic | v | nat |
| m0 | array-copy | v | nat |
| m1 | mtd-base | v | nat |
| m2 | mtd-base | v | nat |
| m3 | avidheader | v | nat |
| m4 | avidheader | v | nat |
| m5 | avidheader | v | nat |
| m6 | avidheader | v | nat |
| max | min-max | f | nat × nat → nat |
| min | min-max | f | nat × nat → nat |
| mkbuf | buffer | f | nat → buffer |
| mkempbuf | buffer | f | nat → buffer |
| mklist | string | f | char × nat → string |
| mkpeb | peb | f | buffer × nat × bool → peb |
| mkpebs | pebs | f | nat → pebs |
| mkzbuf | buffer | f | nat → buffer |
| mtd-cons | mtd-base | p | pebs |
| mtd-valid-peb | mtd-base | p | peb |
| mtd_asm_erase# | mtd-asm | pr | nat : pebs : error (nondeterministic) |
| mtd_asm_get_blockcount# | mtd-asm | pr | pebs : : nat |
| mtd_asm_get_page_size# | mtd-asm | pr | pebs : : nat |
| mtd_asm_get_peb_size# | mtd-asm | pr | pebs : : nat |
| mtd_asm_init# | mtd-asm | pr | : : pebs × error (nondeterministic) |
| mtd_asm_isbad# | mtd-asm | pr | nat × pebs : : bool × error (nondeterministic) |
| mtd_asm_markbad# | mtd-asm | pr | nat : pebs : error (nondeterministic) |
| mtd_asm_read# | mtd-asm | pr | nat × nat × nat × nat × pebs : buffer : bool × error (nondeterministic) |
| mtd_asm_write# | mtd-asm | pr | nat × nat × nat × nat × buffer : pebs : error (nondeterministic) |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| peb | peb | s | |
| peb | peb | v | peb |
| peb0 | pebs | v | peb |
| peb1 | pebs | v | peb |
| pebs | pebs | s | |
| pebs | pebs | v | pebs |
| pebs0 | pebs | v | pebs |
| pebs1 | pebs | v | pebs |
| pebs2 | pebs | v | pebs |
| pos | string | f | char × string → nat |
| range= | buffer | p | buffer × nat × buffer × nat × nat |
| resize | buffer | f | buffer × nat → buffer |
| restn | string | pf | nat × string → string with λ n, str. n ≤ # str |
| rev | pebs | pf | pebs × nat → pebs with λ pebs, n. n ≤ # pebs |
| rev | buffer | f | buffer → buffer |
| rev | buffer | pf | buffer × nat → buffer with λ buf, n. n ≤ # buf |
| rev | string | f | string → string |
| rev | pebs | f | pebs → pebs |
| rmdup | string | f | string → string |
| splice | buffer | f | buffer × nat × buffer × nat × nat → buffer |
| str | string | v | string |
| str0 | string | v | string |
| str1 | string | v | string |
| str2 | string | v | string |
| str3 | string | v | string |
| string | string | s | |
| subarray | pebs | pf | pebs × nat × nat → pebs with λ pebs, m, n. m + n ≤ # pebs |
| 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 |
| ubi-io-initial | ubi-io-base | p | pebs |
| ubi-io-peb-initial | ubi-io-base | p | peb |
| ubi_io_format# | ubi-io-asm | pr | : nat × pebs : error (nondeterministic) |
| ubi_io_get_blockcount# | ubi-io-asm | pr | pebs : : nat |
| ubi_io_get_leb_size# | ubi-io-asm | pr | nat × pebs : : nat |
| ubi_io_get_page_size# | ubi-io-asm | pr | nat : : nat |
| ubi_io_isbad# | ubi-io-asm | pr | nat × pebs : : bool × error (nondeterministic) |
| ubi_io_markbad# | ubi-io-asm | pr | nat : pebs : error (nondeterministic) |
| ubi_io_read# | ubi-io-asm | pr | nat × nat × nat × nat × pebs : buffer : bool × error (nondeterministic) |
| ubi_io_read_data# | ubi-io-asm | pr | nat × nat × nat × nat × nat × pebs : buffer : bool × error (nondeterministic) |
| ubi_io_read_echdr# | ubi-io-asm | pr | nat × nat × pebs : aecheader : bool × error (nondeterministic) |
| ubi_io_read_vidhdr# | ubi-io-asm | pr | nat × nat × pebs : avidheader : bool × error (nondeterministic) |
| ubi_io_recovery# | ubi-io-asm | pr | pebs : : nat |
| ubi_io_sync_erase# | ubi-io-asm | pr | nat : pebs : error (nondeterministic) |
| ubi_io_write_data# | ubi-io-asm | pr | nat × nat × nat × nat × buffer × nat : pebs : error (nondeterministic) |
| ubi_io_write_data_wl# | ubi-io-asm | pr | nat × nat × buffer × nat : pebs : error (nondeterministic) |
| ubi_io_write_echdr# | ubi-io-asm | pr | nat × aecheader × nat : pebs : error (nondeterministic) |
| ubi_io_write_vidhdr# | ubi-io-asm | pr | nat × avidheader × nat : pebs : error (nondeterministic) |
| v | volid | v | volid |
| v0 | volid | v | volid |
| v1 | volid | v | volid |
| v2 | volid | v | volid |
| vhdr | vidheader | v | vidheader |
| vhdr0 | encoding-vidheader | v | vidheader |
| vhdr1 | encoding-vidheader | v | vidheader |
| vidhdr | vidheader | f | volid × nat × nat × nat × nat → vidheader |
| vidheader | vidheader | s | |
| volid | volid | s | |
| zero | buffer | c | data |