[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	buffer	f	buffer → nat
# .	apebs	f	apebs → nat
# .	pebs	f	pebs → nat
# .	string	f	string → 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	apeb	p	apeb
. .bad	peb	p	peb
. .bad:= .	peb	f	peb × bool → peb
. .bad:= .	apeb	f	apeb × bool → apeb
. .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	apeb	f	apeb → buffer
. .data:= .	peb	f	peb × buffer → peb
. .data:= .	apeb	f	apeb × buffer → apeb
. .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
. .echdr	apeb	f	apeb → aecheader
. .echdr:= .	apeb	f	apeb × aecheader → apeb
. .fill	peb	f	peb → nat
. .fill	apeb	f	apeb → nat
. .fill:= .	peb	f	peb × nat → peb
. .fill:= .	apeb	f	apeb × nat → apeb
. .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?	avidheader	p	avidheader
. .valid?	aecheader	p	aecheader
. .vidhdr	apeb	f	apeb → avidheader
. .vidhdr:= .	apeb	f	apeb × avidheader → apeb
. .vol	vidheader	f	vidheader → volid
. .vol	avidheader	pf	avidheader → volid with λ avhdr. avhdr.valid?
. .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
. [ . ]	apebs	pf	apebs × nat × apeb → apebs with λ apebs, n, apeb. n < # apebs
. [ . ]	apebs	pf	apebs × nat → apeb with λ apebs, n. n < # apebs
. [ . ]	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 → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. ∈ .	buffer	p	data × buffer
. ∈ .	apebs	p	apeb × apebs
. ∈ .	pebs	p	peb × pebs
. ∈ .	string	p	char × string
. ≤ .	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	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
BITFLIPS	aubi-io-asm	v	bool,flexible
BUF	aubi-io-asm	v	buffer,flexible
BUF0	aubi-io-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	aubi-io-asm	v	bool,flexible
LEB_SIZE	eraseblock	c	nat
M	ubi-io-asm	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-io-asm	v	nat,flexible
PEB	mtd-asm	v	peb,flexible
PEB_SIZE	eraseblock	c	nat
PEBS	mtd-asm	v	pebs,flexible
PNUM	aubi-io-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
abs	ubi-io-abs	p	pebs × apebs
abs-echdr	ubi-io-abs	p	buffer × aecheader
abs-peb	ubi-io-abs	p	peb × apeb
abs-vidhdr	ubi-io-abs	p	buffer × avidheader
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
bitflips	aubi-io-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	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	pebs	pp	pebs × peb × nat × nat with λ pebs, peb, m, n. m + n ≤ # pebs
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
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
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
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
datasize	datasize	f	buffer → nat
datasize	datasize	f	buffer × nat → nat
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	apebs	pf	apebs × apeb × nat × nat → apebs with λ apebs, apeb, n, m. n + m ≤ # apebs
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
fill	apebs	f	apebs × apeb → apebs
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○	apebs	p	apebs × apebs × nat
id○	buffer	p	buffer × buffer × nat
id○	pebs	p	pebs × pebs × nat
idrange	apebs	pp	apebs × nat × nat with λ apebs, m, n. m + n ≤ # apebs
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
initial-apebs	ubi-io-abs	f	pebs → apebs
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	aubi-io-asm	v	bool
isempty	eraseblock	p	buffer
isempty	eraseblock	p	buffer × nat × nat
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	array-copy	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
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkapebs	apebs	f	nat → apebs
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	string	f	char × nat → string
mkpeb	apeb	f	aecheader × avidheader × buffer × nat × bool → apeb
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
n2	ubi-io-pre	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	apebs	pf	apebs × nat → apebs with λ apebs, n. n ≤ # apebs
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	apebs	f	apebs → apebs
rev	pebs	f	pebs → pebs
rev	string	f	string → string
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	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
subarray	pebs	pf	pebs × nat × nat → pebs with λ pebs, m, n. m + n ≤ # pebs
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
ubi-io-erase-pre	ubi-io-pre	p	nat × apebs
ubi-io-initial	ubi-io-base	p	pebs
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-initial	ubi-io-base	p	peb
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_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