[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,
enrich
inode
,
dentry
,
node-index
,
node-store
,
address-list-set
,
node-list
,
root-ino
,
stringset
,
nat-div
,
error-class
,
key-list-set
with
functions links : nat × node-store × node-index → key-set;
dentries : key × node-index → stringset;
dentrykeys : key × node-index → key-set;
datakeys : key × node-index → key-set;
datakeys : key × nat × node-index → key-set;
datakeys : key-set × node-index → key-set;
. ⊖ . : node-index × key → node-index;
. ⊖ . : node-index × key-set → node-index;
. [ . ] : node-index × key-list × address-list → node-index;
. [ . ] : node-index × key-list → address-list;
. [ . ] : node-store × address-list × node-list → node-store;
. [ . ] : node-store × address-list → node-list;
keys : node-store × address-list → key-list;
range . : node-index → address-set;
predicates valid-ino : nat × node-store × node-index;
valid-dir-ino : nat × node-store × node-index;
valid-parent-ino : nat × node-store × node-index × key-set;
valid-file-ino : nat × node-store × node-index;
valid-dentry : dentry × node-store × node-index × key-set;
valid-dentry : nat × dentry × node-store × node-index × key-set;
valid-negdentry : nat × dentry × node-store × node-index × key-set;
aubifs-crash
: node-index × key-set × key-set × node-index × key-set × node-store × address-list × node-index × key-set × key-set × node-index ×
key-set × node-store × address-list
;
new : address-list × node-store;
variables fi : node-index;
fi0 : node-index;
fi1 : node-index;
fi2 : node-index;
log : address-list;
log0 : address-list;
log1 : address-list;
log2 : address-list;
ino : nat;
ino0 : nat;
ino1 : nat;
ino2 : nat;
ro : key-set;
ro0 : key-set;
ro1 : key-set;
ro2 : key-set;
fo : key-set;
fo0 : key-set;
fo1 : key-set;
fo2 : key-set;
ld : key-set;
ld0 : key-set;
ld1 : key-set;
ld2 : key-set;
axioms new-base : ⊦ new([], fs);
used for: s, ls;
new-rec : ⊦ new(adr ' + log, fs) ↔ ¬ adr ∈ fs ∧ new(log, fs);
used for: s, ls;
links : ⊦ key ∈ links(ino, fs, ri) ↔ key ∈ ri ∧ key.dentry? ∧ fs[ri[key]].ino = ino;
used for: s, ls;
del-with-data : ⊦ ri ⊖ key = (ri -- key) \ datakeys(key, ri);
dels-with-data : ⊦ ri ⊖ ks = (ri \ ks) \ datakeys(ks, ri);
dentries : ⊦ str ∈ dentries(key, ri) ↔ dentrykey(key.ino, str) ∈ dentrykeys(key, ri);
used for: s, ls;
dentrykeys : ⊦ key ∈ dentrykeys(key0, ri) ↔ key ∈ ri ∧ key.dentry? ∧ key0.inode? ∧ key.ino = key0.ino;
used for: s, ls;
datakeys : ⊦ key ∈ datakeys(key0, ri) ↔ key ∈ ri ∧ key.data? ∧ key0.inode? ∧ key.ino = key0.ino;
used for: s, ls;
datakeys-ge : ⊦ key ∈ datakeys(key0, n, ri) ↔ key ∈ datakeys(key0, ri) ∧ n ≤ key.part * VFS_PAGE_SIZE;
used for: s, ls;
datakeys-set : ⊦ key ∈ datakeys(ks, ri) ↔ key ∈ ri ∧ key.data? ∧ inodekey(key.ino) ∈ ks;
used for: s, ls;
valid-ino : ⊦ valid-ino(ino, fs, ri) ↔ inodekey(ino) ∈ ri;
used for: s, ls;
valid-file-ino : ⊦ valid-file-ino(ino, fs, ri) ↔ inodekey(ino) ∈ ri ∧ ¬ fs[ri[inodekey(ino)]].directory;
used for: s, ls;
valid-dir-ino : ⊦ valid-dir-ino(ino, fs, ri) ↔ inodekey(ino) ∈ ri ∧ fs[ri[inodekey(ino)]].directory;
used for: s, ls;
valid-parent-ino
: ⊦ valid-parent-ino(ino, fs, ri, ro)
↔ (valid-dir-ino(ino, fs, ri) ∧ (fs[ri[inodekey(ino)]].nlink ≠ 0 ∨ ino = ROOT_INO)) ∧ ¬ inodekey(ino) ∈ ro;
used for: s, ls;
valid-dentry : ⊦ valid-dentry(dent, fs, ri, ro) ↔ (∃ ino. valid-dentry(ino, dent, fs, ri, ro));
used for: s, ls;
valid-dentry-with-parent
: ⊦ valid-dentry(ino, dent, fs, ri, ro)
↔ dent.dentry? ∧ valid-parent-ino(ino, fs, ri, ro) ∧ valid-ino(dent.ino, fs, ri) ∧ dentrykey(ino, dent.name) ∈ ri
∧ fs[ri[dentrykey(ino, dent.name)]].ino = dent.ino;
used for: s, ls;
valid-negdentry-with-parent
: ⊦ valid-negdentry(ino, dent, fs, ri, ro) ↔ dent.negdentry? ∧ valid-parent-ino(ino, fs, ri, ro) ∧ ¬ dentrykey(ino, dent.name) ∈ ri;
used for: s, ls;
index-update-key-base : ⊦ ri[[], []] = ri;
used for: s, ls;
index-update-key-rec : ⊦ ri[key ' + kx, adr ' + ax] = ri[key, adr][kx, ax];
used for: s, ls;
index-lookup-base : ⊦ ri[[]] = [];
used for: s, ls;
index-lookup-rec : ⊦ ri[key ' + kx] = ri[key] + ri[kx];
used for: s, ls;
keys-base : ⊦ keys(fs, []) = [];
used for: s, ls;
keys-rec : ⊦ keys(fs, adr ' + ax) = fs[adr].key + keys(fs, ax);
used for: s, ls;
range : ⊦ adr ∈ range ri ↔ adr ∈ ri;
used for: s, ls;
aubifs-crash
: ⊦ aubifs-crash(ri0, ld0, ro0, fi0, fo0, fs0, log0, ri1, ld1, ro1, fi1, fo1, fs1, log1) ↔ fi1 = fi0 ∧ fo1 = fo0 ∧ fs1 = fs0 ∧ log1 = log0;
write-base : ⊦ fs[[], []] = fs;
used for: s, ls;
write-rec : ⊦ fs[adr ' + ax, nd ' + ndx] = fs[adr, nd][ax, ndx];
used for: s, ls;
read-base : ⊦ fs[[]] = [];
used for: s, ls;
read-rec : ⊦ fs[adr ' + ax] = fs[adr] + fs[ax];
used for: s, ls;
end enrich