[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
# .	erasequeue-base	f	queue → nat
# .	lebrefset	f	lebrefset → nat
# .	buffer	f	buffer → nat
# .	apebs	f	apebs → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	erasequeue-base	f	erasequeueentry → queue
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	erasequeue-base	f	erasequeueentry × queue → queue
. + .	erasequeue-base	f	queue × erasequeueentry → queue
. + .	erasequeue-base	f	queue × queue → queue
. ++ .	lebrefset	f	lebrefset × lebref → lebrefset
. ++ .	erasequeue-base	f	queue × erasequeueentry → queue
. +1	nat-basic	f	nat → nat
. +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
. -- .	lebrefset	f	lebrefset × lebref → lebrefset
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	erasequeue-base	f	queue × erasequeueentry → queue
. -l .	erasequeue-base	f	queue × erasequeueentry → queue
. -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 ≠ []
. .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	aecheader	pf	aecheader → nat with λ aehdr. aehdr.valid?
. .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
. .head	erasequeue-base	pf	queue → erasequeueentry with λ q. q ≠ []
. .last	erasequeue-base	pf	queue → erasequeueentry with λ q. q ≠ []
. .leb	avidheader	pf	avidheader → nat with λ avhdr. avhdr.valid?
. .leb	lebref	pf	lebref → nat with λ lref. lref ≠ none
. .leb:= .	avidheader	pf	avidheader × nat → avidheader with λ avhdr, m. avhdr.valid?
. .leb:= .	lebref	pf	lebref × nat → lebref with λ lref, m. lref ≠ none
. .lebref	erasequeueentry	f	erasequeueentry → lebref
. .lebref:= .	erasequeueentry	f	erasequeueentry × lebref → erasequeueentry
. .lebrefs	erasequeue	f	queue → lebrefset
. .pnum	erasequeueentry	f	erasequeueentry → nat
. .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?
. .tail	erasequeue-base	pf	queue → queue with λ q. q ≠ []
. .valid?	aecheader	p	aecheader
. .valid?	avidheader	p	avidheader
. .vidhdr	apeb	f	apeb → avidheader
. .vidhdr:= .	apeb	f	apeb × avidheader → apeb
. .vol	avidheader	pf	avidheader → volid with λ avhdr. avhdr.valid?
. .vol	lebref	pf	lebref → volid with λ lref. lref ≠ none
. .vol:= .	avidheader	pf	avidheader × volid → avidheader with λ avhdr, v. avhdr.valid?
. .vol:= .	lebref	pf	lebref × volid → lebref with λ lref, v. lref ≠ none
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	erasequeue-base	p	queue × queue
. > .	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
. [ . ]	erasequeue-base	pf	queue × nat → erasequeueentry with λ q, n. n < # q
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	erasequeue-base	pf	queue × nat × erasequeueentry → queue with λ q, n, eqent. n < # q
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. \ .	erasequeue-base	f	queue × queue → queue
. \ .	lebrefset	f	lebrefset × lebrefset → lebrefset
. × .	lebref	f	volid × nat → lebref
. ∈ .	erasequeue	p	volid × queue
. ∈ .	erasequeue	p	lebref × queue
. ∈ .	erasequeue	p	nat × queue
. ∈ .	erasequeue-base	p	erasequeueentry × queue
. ∈ .	lebrefset	p	lebref × lebrefset
. ∈ .	buffer	p	data × buffer
. ∈ .	apebs	p	apeb × apebs
. ∩ .	lebrefset	f	lebrefset × lebrefset → lebrefset
. ∪ .	erasequeue-base	f	queue × queue → queue
. ∪ .	lebrefset	f	lebrefset × lebrefset → lebrefset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	lebrefset	p	lebrefset × lebrefset
. ⊆ .	erasequeue-base	p	queue × queue
. ⊑ .	erasequeue-base	p	queue × queue
. ⊒ .	erasequeue-base	p	queue × queue
[]	erasequeue-base	c	queue
{ . }	lebrefset	f	lebref → lebrefset
∅	lebrefset	c	lebrefset
⌊ . ⌋	error-class	p	error
EACCESS	error	c	error
EB_PAGE_SIZE	eraseblock	c	nat
EBADFD	error	c	error
ECOMMIT	error	c	error
EEXISTS	error	c	error
EFAIL	error	c	error
EINVAL	error	c	error
EIO	error	c	error
EISDIR	error	c	error
ENOENT	error	c	error
ENOMEM	error	c	error
ENOSPC	error	c	error
ENOTDIR	error	c	error
ENOTEMPTY	error	c	error
EROFS	error	c	error
ERR	error-class	v	error,flexible
ERR0	error-class	v	error,flexible
ESUCCESS	error	c	error
EUCLEAN	error	c	error
LEB_SIZE	eraseblock	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
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
bool	bool	s
boolvar	bool	v	bool
boolvar0	bool	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
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	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	apebs	pf	apebs × nat × apebs × nat × nat → apebs with λ apebs, m, apebs0, m0, n. m + n ≤ # apebs ∧ m0 + n ≤ # apebs0
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
disj	erasequeue-base	p	queue × queue
dups	erasequeue-base	p	queue
empty	aecheader	c	aecheader
empty	buffer	c	data
empty	avidheader	c	avidheader
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
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
erasequeueentry	erasequeueentry	s
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	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	apebs	f	apebs × apeb → apebs
fill	buffer	f	buffer × data → buffer
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
frome	erasequeue-base	f	queue × erasequeueentry → queue
garbage	aecheader	c	aecheader
garbage	avidheader	c	avidheader
id○	apebs	p	apebs × apebs × nat
id○	buffer	p	buffer × buffer × nat
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
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer
isempty	eraseblock	p	buffer × nat × nat
lastn	erasequeue-base	pf	nat × queue → queue with λ n, q. n ≤ # q
lebref	lebref	s
lebrefset	lebrefset	s
lref	lebref	v	lebref
lref0	lebrefset	v	lebref
lref1	lebrefset	v	lebref
m	nat-basic	v	nat
m0	lebref	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	erasequeue-base	f	erasequeueentry × nat → queue
mkpeb	apeb	f	aecheader × avidheader × buffer × nat × bool → apeb
mkzbuf	buffer	f	nat → buffer
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
none	lebref	c	lebref
pos	erasequeue-base	f	erasequeueentry × queue → nat
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
rev	apebs	pf	apebs × nat → apebs with λ apebs, n. n ≤ # apebs
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	erasequeue-base	f	queue → queue
rev	apebs	f	apebs → apebs
rev	buffer	f	buffer → buffer
rmdup	erasequeue-base	f	queue → queue
s	lebrefset	v	lebrefset
s0	lebrefset	v	lebrefset
s1	lebrefset	v	lebrefset
s2	lebrefset	v	lebrefset
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
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	erasequeue-base	pf	nat × nat × queue → queue with λ n, m, q. n + m ≤ # q
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
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
valid-peb	valid-peb	p	volid × nat × apeb
valid-peb	valid-peb	p	apeb
volid	volid	s
zero	buffer	c	data