Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(635 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(36 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(30 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(132 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(60 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(159 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(22 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(23 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(153 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Global Index

A

Abstraction [definition, in POCS.Spec.Abstraction]
abstraction [projection, in POCS.Spec.Abstraction]
Abstraction [library]
abstraction_compose [definition, in POCS.Spec.Abstraction]
addr [definition, in POCS.Helpers.Disk]
addr_to_block_ok [axiom, in POCS.Lab3.LogImpl]
addr_to_block_spec [definition, in POCS.Lab3.LogImpl]
addr_to_block [axiom, in POCS.Lab3.LogImpl]
add_spec [definition, in POCS.Lab1.StatDbAPI]
append_spec [definition, in POCS.Lab3.LogAPI]

B

BadBlockAPI [module, in POCS.Lab2.BadBlockAPI]
BadBlockAPI [library]
BadBlockAPI.abstr [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover_wipe [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockDisk [module, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.abstr [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover_wipe [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockImpl [library]
bad_disk [module, in POCS.Lab3.LogImpl]
bappend [axiom, in POCS.Helpers.Disk]
baseModel [axiom, in POCS.Spec.Proc]
BaseOp [constructor, in POCS.Spec.Proc]
baseOpT [definition, in POCS.Spec.Proc]
base_step [definition, in POCS.Spec.Proc]
bg_failure [inductive, in POCS.Lab4.TwoDiskBaseAPI]
Bind [constructor, in POCS.Spec.Proc]
block [definition, in POCS.Helpers.Disk]
blockbytes [definition, in POCS.Helpers.Disk]
block_to_addr [axiom, in POCS.Lab3.LogImpl]
block0 [definition, in POCS.Helpers.Disk]
block0_block1_differ [lemma, in POCS.Helpers.Disk]
block1 [definition, in POCS.Helpers.Disk]
bnull [definition, in POCS.Helpers.Disk]
bool_equal_dec [instance, in POCS.Helpers.Helpers]
BothDisks [constructor, in POCS.Lab4.TwoDiskBaseAPI]
bsplit [axiom, in POCS.Helpers.Disk]
bsplit_list [definition, in POCS.Helpers.Disk]
bsplit_bappend [axiom, in POCS.Helpers.Disk]
bytes [axiom, in POCS.Helpers.Disk]
bytes_differ [axiom, in POCS.Helpers.Disk]
bytes_dec [axiom, in POCS.Helpers.Disk]
bytes0 [axiom, in POCS.Helpers.Disk]
bytes1 [axiom, in POCS.Helpers.Disk]

C

cli [definition, in POCS.Lab1.StatDbCli]
clos_refl_trans_1n_unit_tuple [lemma, in POCS.Spec.Recovery]
combined_step [definition, in POCS.Lab4.TwoDiskBaseAPI]
compose_recovery [lemma, in POCS.Spec.Recovery]
Crashed [constructor, in POCS.Spec.Proc]

D

d [module, in POCS.Lab2.RemappedServer]
data [projection, in POCS.Common.NbdAPI]
data_len [projection, in POCS.Common.NbdAPI]
DeexTests [module, in POCS.Helpers.Helpers]
DeexTests.chooses_fresh_name [lemma, in POCS.Helpers.Helpers]
DeexTests.chooses_name [lemma, in POCS.Helpers.Helpers]
DestructMatchesTests [module, in POCS.Helpers.Helpers]
DestructMatchesTests.destructs_innermost_match [lemma, in POCS.Helpers.Helpers]
DestructMatchesTests.removes_absurdities [lemma, in POCS.Helpers.Helpers]
Disconnect [constructor, in POCS.Common.NbdAPI]
disk [definition, in POCS.Helpers.Disk]
Disk [library]
diskGet [definition, in POCS.Helpers.Disk]
diskGets [definition, in POCS.Helpers.Disk]
diskGets_app [lemma, in POCS.Helpers.Disk]
diskGets_last [lemma, in POCS.Helpers.Disk]
diskGets_first [lemma, in POCS.Helpers.Disk]
diskGet_eq_values [lemma, in POCS.Lab3.LogImpl]
diskId [inductive, in POCS.Lab4.TwoDiskBaseAPI]
DiskResult [inductive, in POCS.Lab4.TwoDiskBaseAPI]
diskShrink [definition, in POCS.Helpers.Disk]
diskShrink_diskUpd_notlast [lemma, in POCS.Helpers.Disk]
diskShrink_diskUpd_last [lemma, in POCS.Helpers.Disk]
diskShrink_preserves [lemma, in POCS.Helpers.Disk]
diskShrink_size [lemma, in POCS.Helpers.Disk]
diskSize [definition, in POCS.Helpers.Disk]
diskUpd [definition, in POCS.Helpers.Disk]
diskUpds [definition, in POCS.Helpers.Disk]
diskUpds_diskGets_eq [lemma, in POCS.Helpers.Disk]
diskUpds_diskGets_neq [lemma, in POCS.Helpers.Disk]
diskUpds_diskUpd_before [lemma, in POCS.Helpers.Disk]
diskUpds_diskUpd_after [lemma, in POCS.Helpers.Disk]
diskUpds_diskUpd_comm [lemma, in POCS.Helpers.Disk]
diskUpds_size [lemma, in POCS.Helpers.Disk]
diskUpds_neq [lemma, in POCS.Helpers.Disk]
diskUpd_diskGets_neq [lemma, in POCS.Helpers.Disk]
diskUpd_oob_noop [lemma, in POCS.Helpers.Disk]
diskUpd_comm_lt [lemma, in POCS.Helpers.Disk]
diskUpd_comm [lemma, in POCS.Helpers.Disk]
diskUpd_twice [lemma, in POCS.Helpers.Disk]
diskUpd_same [lemma, in POCS.Helpers.Disk]
diskUpd_none [lemma, in POCS.Helpers.Disk]
diskUpd_neq [lemma, in POCS.Helpers.Disk]
diskUpd_oob_eq [lemma, in POCS.Helpers.Disk]
diskUpd_size [lemma, in POCS.Helpers.Disk]
diskUpd_eq [lemma, in POCS.Helpers.Disk]
diskUpd_eq_some [lemma, in POCS.Helpers.Disk]
disk_ext_inbounds_eq [lemma, in POCS.Helpers.Disk]
disk_ext_eq [lemma, in POCS.Helpers.Disk]
disk_oob_eq [lemma, in POCS.Helpers.Disk]
disk_none_oob [lemma, in POCS.Helpers.Disk]
disk_inbounds_not_none [lemma, in POCS.Helpers.Disk]
disk_inbounds_exists [lemma, in POCS.Helpers.Disk]
disk0 [definition, in POCS.Lab4.TwoDiskBaseAPI]
disk1 [definition, in POCS.Lab4.TwoDiskBaseAPI]
d0 [constructor, in POCS.Lab4.TwoDiskBaseAPI]
d1 [constructor, in POCS.Lab4.TwoDiskBaseAPI]

E

EInvalid [constructor, in POCS.Common.NbdAPI]
empty_disk [definition, in POCS.Helpers.Disk]
ENospc [constructor, in POCS.Common.NbdAPI]
EqualDec [record, in POCS.Helpers.Helpers]
EqualDec [inductive, in POCS.Helpers.Helpers]
equal_dec [projection, in POCS.Helpers.Helpers]
equal_dec [constructor, in POCS.Helpers.Helpers]
error [projection, in POCS.Common.NbdAPI]
ErrorCode [inductive, in POCS.Common.NbdAPI]
ESuccess [constructor, in POCS.Common.NbdAPI]
exec [inductive, in POCS.Spec.Proc]
ExecBindCrashed [constructor, in POCS.Spec.Proc]
ExecBindFinished [constructor, in POCS.Spec.Proc]
ExecCrashBegin [constructor, in POCS.Spec.Proc]
ExecCrashEnd [constructor, in POCS.Spec.Proc]
ExecOp [constructor, in POCS.Spec.Proc]
ExecRecoverCrashDuringRecovery [constructor, in POCS.Spec.Proc]
ExecRecoverExec [constructor, in POCS.Spec.Proc]
ExecRet [constructor, in POCS.Spec.Proc]
exec_recover [inductive, in POCS.Spec.Proc]
exec_recover_bind_inv [lemma, in POCS.Spec.ProcTheorems]
exec_equiv_equiv [instance, in POCS.Spec.ProcTheorems]
exec_equiv [definition, in POCS.Spec.ProcTheorems]
exec_ret [lemma, in POCS.Spec.ProcTheorems]
Exercises [module, in POCS.Lab0.Exercises]
Exercises [library]
Exercises.addX [definition, in POCS.Lab0.Exercises]
Exercises.addX_list_ok [lemma, in POCS.Lab0.Exercises]
Exercises.addX_list [definition, in POCS.Lab0.Exercises]
Exercises.addX_ok [lemma, in POCS.Lab0.Exercises]
Exercises.add_odds_evens_ok_seems_good [lemma, in POCS.Lab0.Exercises]
Exercises.add_odds_evens [definition, in POCS.Lab0.Exercises]
Exercises.incX [definition, in POCS.Lab0.Exercises]
Exercises.incX_ok_seems_good [lemma, in POCS.Lab0.Exercises]
Exercises.incX_ok [lemma, in POCS.Lab0.Exercises]
Exercises.incX_test [lemma, in POCS.Lab0.Exercises]
Exercises.list_sum [definition, in POCS.Lab0.Exercises]
Exercises.swapXY [definition, in POCS.Lab0.Exercises]
Exercises.swapXY_ok_seems_good [lemma, in POCS.Lab0.Exercises]
Exercises.swapXY_ok [lemma, in POCS.Lab0.Exercises]

F

Failed [constructor, in POCS.Lab4.TwoDiskBaseAPI]
Finished [constructor, in POCS.Spec.Proc]
Flush [constructor, in POCS.Common.NbdAPI]

G

getBadBlock_spec [definition, in POCS.Lab2.BadBlockAPI]
getRequest_spec [definition, in POCS.Common.NbdAPI]
get_new_item [axiom, in POCS.Lab1.StatDbCli]
get_disk [definition, in POCS.Lab4.TwoDiskBaseAPI]
get_spec [definition, in POCS.Lab3.LogAPI]

H

Handle [axiom, in POCS.Common.NbdAPI]
Helpers [library]
holds_some_inv_eq [lemma, in POCS.Helpers.Helpers]
holds_in_some_eq [lemma, in POCS.Helpers.Helpers]
holds_in_some [lemma, in POCS.Helpers.Helpers]
holds_in_none_eq [lemma, in POCS.Helpers.Helpers]

I

IdAbstraction [definition, in POCS.Spec.Abstraction]
idempotent [definition, in POCS.Spec.Recovery]
idempotent_loopspec [lemma, in POCS.Spec.Recovery]
init [definition, in POCS.Lab4.ReplicatedServer]
init [definition, in POCS.Lab2.RemappedServer]
inited [definition, in POCS.Lab1.StatDbAPI]
inited [definition, in POCS.Common.NbdAPI]
inited_any [definition, in POCS.Spec.Abstraction]
InitFailed [constructor, in POCS.Spec.Abstraction]
Initialized [constructor, in POCS.Spec.Abstraction]
InitResult [inductive, in POCS.Spec.Abstraction]
init_abstraction_any_rec [lemma, in POCS.Spec.Abstraction]
init_abstraction [definition, in POCS.Spec.Abstraction]
IO [module, in POCS.Spec.Proc]
IO.baseOpT [projection, in POCS.Spec.Proc]
IO.base_step [projection, in POCS.Spec.Proc]
IO.Model [record, in POCS.Spec.Proc]
IO.world [projection, in POCS.Spec.Proc]
IO.world_crash [projection, in POCS.Spec.Proc]

L

LayerAbstraction [record, in POCS.Spec.Abstraction]
log [module, in POCS.Lab3.LogImpl]
Log [module, in POCS.Lab3.LogImpl]
LogAPI [module, in POCS.Lab3.LogAPI]
LogAPI [library]
LogAPI.abstr [axiom, in POCS.Lab3.LogAPI]
LogAPI.append [axiom, in POCS.Lab3.LogAPI]
LogAPI.append_ok [axiom, in POCS.Lab3.LogAPI]
LogAPI.get [axiom, in POCS.Lab3.LogAPI]
LogAPI.get_ok [axiom, in POCS.Lab3.LogAPI]
LogAPI.init [axiom, in POCS.Lab3.LogAPI]
LogAPI.init_ok [axiom, in POCS.Lab3.LogAPI]
LogAPI.recover [axiom, in POCS.Lab3.LogAPI]
LogAPI.recover_wipe [axiom, in POCS.Lab3.LogAPI]
LogAPI.reset [axiom, in POCS.Lab3.LogAPI]
LogAPI.reset_ok [axiom, in POCS.Lab3.LogAPI]
LogImpl [library]
Log.abstr [axiom, in POCS.Lab3.LogImpl]
Log.append [definition, in POCS.Lab3.LogImpl]
Log.append_ok [axiom, in POCS.Lab3.LogImpl]
Log.get [definition, in POCS.Lab3.LogImpl]
Log.get_ok [axiom, in POCS.Lab3.LogImpl]
Log.init [definition, in POCS.Lab3.LogImpl]
Log.init_ok [axiom, in POCS.Lab3.LogImpl]
Log.recover [definition, in POCS.Lab3.LogImpl]
Log.recover_wipe [axiom, in POCS.Lab3.LogImpl]
Log.reset [definition, in POCS.Lab3.LogImpl]
Log.reset_ok [axiom, in POCS.Lab3.LogImpl]
loop [definition, in POCS.Lab1.StatDbCli]

M

mark [constructor, in POCS.Spec.Abstraction]
Marker [inductive, in POCS.Spec.Abstraction]
maybe_eq_list_map_some [lemma, in POCS.Helpers.Helpers]
maybe_eq_list_app [lemma, in POCS.Helpers.Helpers]
maybe_eq_list_last [lemma, in POCS.Helpers.Helpers]
maybe_eq_list_last_helper [lemma, in POCS.Helpers.Helpers]
maybe_eq_list_len [lemma, in POCS.Helpers.Helpers]
maybe_eq_list_first [lemma, in POCS.Helpers.Helpers]
maybe_eq_list [definition, in POCS.Helpers.Helpers]
maybe_eq [definition, in POCS.Helpers.Helpers]
maybe_holds [definition, in POCS.Helpers.Helpers]
maybe_eq_None_holds [lemma, in POCS.Helpers.Disk]
maybe_eq_None_is_True [lemma, in POCS.Helpers.Disk]
mean_spec [definition, in POCS.Lab1.StatDbAPI]
missing [definition, in POCS.Helpers.Helpers]
mkState [constructor, in POCS.Common.NbdAPI]
mkState [constructor, in POCS.Lab1.VariablesAPI]
mkState [constructor, in POCS.Lab2.BadBlockAPI]
mkState [constructor, in POCS.Lab0.ThreeVariablesAPI]
monad_assoc [lemma, in POCS.Spec.ProcTheorems]
monad_left_id [lemma, in POCS.Spec.ProcTheorems]

N

nat_equal_dec [instance, in POCS.Helpers.Helpers]
nbd [module, in POCS.Common.NbdServer]
NbdAPI [module, in POCS.Common.NbdAPI]
NbdAPI [library]
NbdAPI.abstr [axiom, in POCS.Common.NbdAPI]
NbdAPI.getRequest [axiom, in POCS.Common.NbdAPI]
NbdAPI.getRequest_ok [axiom, in POCS.Common.NbdAPI]
NbdAPI.init [axiom, in POCS.Common.NbdAPI]
NbdAPI.init_ok [axiom, in POCS.Common.NbdAPI]
NbdAPI.recover [axiom, in POCS.Common.NbdAPI]
NbdAPI.recover_wipe [axiom, in POCS.Common.NbdAPI]
NbdAPI.sendResponse [axiom, in POCS.Common.NbdAPI]
NbdAPI.sendResponse_ok [axiom, in POCS.Common.NbdAPI]
NbdImpl [module, in POCS.Common.NbdImpl]
NbdImpl [library]
NbdImpl.abstr [axiom, in POCS.Common.NbdImpl]
NbdImpl.getRequest [axiom, in POCS.Common.NbdImpl]
NbdImpl.getRequest_ok [axiom, in POCS.Common.NbdImpl]
NbdImpl.init [axiom, in POCS.Common.NbdImpl]
NbdImpl.init_ok [axiom, in POCS.Common.NbdImpl]
NbdImpl.recover [axiom, in POCS.Common.NbdImpl]
NbdImpl.recover_wipe [axiom, in POCS.Common.NbdImpl]
NbdImpl.sendResponse [axiom, in POCS.Common.NbdImpl]
NbdImpl.sendResponse_ok [axiom, in POCS.Common.NbdImpl]
NBDServer [module, in POCS.Common.NbdServer]
NbdServer [library]
NBDServer.handle [definition, in POCS.Common.NbdServer]
NBDServer.init [definition, in POCS.Common.NbdServer]
NBDServer.read [definition, in POCS.Common.NbdServer]
NBDServer.read_ok [lemma, in POCS.Common.NbdServer]
NBDServer.serverLoop [definition, in POCS.Common.NbdServer]
NBDServer.size [definition, in POCS.Common.NbdServer]
NBDServer.write [definition, in POCS.Common.NbdServer]
NBDServer.write_ok [lemma, in POCS.Common.NbdServer]
no_crash [definition, in POCS.Spec.Recovery]
no_wipe [definition, in POCS.Spec.Recovery]

O

OneDiskAPI [module, in POCS.Common.OneDiskAPI]
OneDiskAPI [library]
OneDiskAPI.abstr [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.init [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.init_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.read [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.read_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.recover [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.recover_wipe [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.size [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.size_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.write [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.write_ok [axiom, in POCS.Common.OneDiskAPI]
OnlyDisk0 [constructor, in POCS.Lab4.TwoDiskBaseAPI]
OnlyDisk1 [constructor, in POCS.Lab4.TwoDiskBaseAPI]
Op [inductive, in POCS.Lab4.TwoDiskBaseAPI]
op_spec [definition, in POCS.Spec.Recovery]
op_step [inductive, in POCS.Lab4.TwoDiskBaseAPI]
op_size [constructor, in POCS.Lab4.TwoDiskBaseAPI]
op_write [constructor, in POCS.Lab4.TwoDiskBaseAPI]
op_read [constructor, in POCS.Lab4.TwoDiskBaseAPI]

P

POCS [library]
post [projection, in POCS.Spec.Abstraction]
post_step [definition, in POCS.Spec.Recovery]
pre [projection, in POCS.Spec.Abstraction]
pred_missing [lemma, in POCS.Helpers.Helpers]
pred_weaken [lemma, in POCS.Helpers.Helpers]
pre_step [definition, in POCS.Spec.Recovery]
proc [inductive, in POCS.Spec.Proc]
Proc [library]
ProcTheorems [library]
proc_loopspec [definition, in POCS.Spec.Recovery]
proc_spec_rx [lemma, in POCS.Spec.Abstraction]
proc_spec_implication [lemma, in POCS.Spec.Abstraction]
proc_spec_weaken [lemma, in POCS.Spec.Abstraction]
proc_spec [definition, in POCS.Spec.Abstraction]

R

rd [module, in POCS.Lab4.ReplicatedServer]
Read [constructor, in POCS.Common.NbdAPI]
read_spec [definition, in POCS.Common.OneDiskAPI]
read_match' [definition, in POCS.Common.NbdAPI]
read_match [definition, in POCS.Common.NbdAPI]
read_spec [definition, in POCS.Lab1.VariablesAPI]
read_spec [definition, in POCS.Lab2.BadBlockAPI]
read_spec [definition, in POCS.Lab0.ThreeVariablesAPI]
read0_spec [definition, in POCS.Lab4.TwoDiskAPI]
read1_spec [definition, in POCS.Lab4.TwoDiskAPI]
Recovered [constructor, in POCS.Spec.Proc]
recovered [projection, in POCS.Spec.Abstraction]
Recovery [library]
rec_wipe_compose [lemma, in POCS.Spec.Recovery]
rec_wipe [definition, in POCS.Spec.Abstraction]
RemappedDisk [module, in POCS.Lab2.RemappedDiskImpl]
RemappedDiskImpl [library]
RemappedDisk.abstr [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_5_nok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_4_nok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_3_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_2_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_1_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.bad_block_inbounds [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init' [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover_wipe [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.RemappedAbstraction [constructor, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_noremap [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_remap [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction [inductive, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedServer [library]
remapped_disk [module, in POCS.Lab3.LogImpl]
ReplicatedDisk [module, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDiskImpl [library]
ReplicatedDisk.abstr [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.both_disks_not_missing [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Continue [constructor, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.DiskStatus [inductive, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.disks_eq_inbounds [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.diskUpd_maybe_same [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_size [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_0_to_eq [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_diskUpd [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.exists_tuple2 [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.fixup [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.fixup_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.FullySynced [constructor, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.if_lt_dec [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_at_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_at [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init' [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init'_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.le_eq_or_S_le [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.missing0_implies_any [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.missing1_implies_any [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.OutOfSync [constructor, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.rd_abstraction [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read_int_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_wipe [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_spec_idempotent [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_rok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_spec [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_at_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_at [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.RecStatus [inductive, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.RepairDoneOrFailed [constructor, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.sizeInit [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.sizeInit_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size_int_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write [definition, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write_int_ok [lemma, in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedServer [library]
report_mean [axiom, in POCS.Lab1.StatDbCli]
Request [inductive, in POCS.Common.NbdAPI]
reset_spec [definition, in POCS.Lab3.LogAPI]
Response [record, in POCS.Common.NbdAPI]
Result [inductive, in POCS.Spec.Proc]
Ret [constructor, in POCS.Spec.Proc]
ret_spec [lemma, in POCS.Spec.Abstraction]
RExec [constructor, in POCS.Spec.Proc]
rexec [inductive, in POCS.Spec.Proc]
RExecCrash [constructor, in POCS.Spec.Proc]
rexec_finish_any_rec [lemma, in POCS.Spec.ProcTheorems]
rexec_equiv [lemma, in POCS.Spec.ProcTheorems]
RFinished [constructor, in POCS.Spec.Proc]
rhandle [projection, in POCS.Common.NbdAPI]
RResult [inductive, in POCS.Spec.Proc]

S

s [module, in POCS.Lab4.ReplicatedServer]
s [module, in POCS.Lab2.RemappedServer]
Semantics [definition, in POCS.Spec.Recovery]
sendResponse_spec [definition, in POCS.Common.NbdAPI]
serverLoop [definition, in POCS.Lab4.ReplicatedServer]
serverLoop [definition, in POCS.Lab2.RemappedServer]
set_disk [definition, in POCS.Lab4.TwoDiskBaseAPI]
SimplMatchTests [module, in POCS.Helpers.Helpers]
SimplMatchTests.fails_on_hyp_if_match_not_removed [lemma, in POCS.Helpers.Helpers]
SimplMatchTests.fails_if_match_not_removed [lemma, in POCS.Helpers.Helpers]
SimplMatchTests.removes_match [lemma, in POCS.Helpers.Helpers]
size [definition, in POCS.Lab4.ReplicatedServer]
size [definition, in POCS.Lab2.RemappedServer]
size_spec [definition, in POCS.Common.OneDiskAPI]
size_spec [definition, in POCS.Lab2.BadBlockAPI]
size0_spec [definition, in POCS.Lab4.TwoDiskAPI]
size1_spec [definition, in POCS.Lab4.TwoDiskAPI]
Spec [constructor, in POCS.Spec.Abstraction]
Specification [definition, in POCS.Spec.Abstraction]
SpecProps [record, in POCS.Spec.Abstraction]
spec_abstraction_compose [lemma, in POCS.Spec.Abstraction]
spec_exec_equiv [lemma, in POCS.Spec.Abstraction]
spec_intros [lemma, in POCS.Spec.Abstraction]
spec_impl [definition, in POCS.Spec.Abstraction]
statdb [module, in POCS.Lab1.StatDbCli]
StatDB [module, in POCS.Lab1.StatDbImpl]
StatDbAPI [module, in POCS.Lab1.StatDbAPI]
StatDbAPI [library]
StatDbAPI.abstr [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.add [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.add_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.init [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.init_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.mean [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.mean_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.recover [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.recover_wipe [axiom, in POCS.Lab1.StatDbAPI]
StatDbCli [library]
StatDBImpl [module, in POCS.Lab1.StatDbImpl]
StatDbImpl [library]
StatDB.abstr [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_5_nok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_4_nok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_3_ok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_2_ok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_1_ok [definition, in POCS.Lab1.StatDbImpl]
StatDB.add [definition, in POCS.Lab1.StatDbImpl]
StatDB.add_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.init [definition, in POCS.Lab1.StatDbImpl]
StatDB.init_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.init' [definition, in POCS.Lab1.StatDbImpl]
StatDB.mean [definition, in POCS.Lab1.StatDbImpl]
StatDB.mean_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.recover [definition, in POCS.Lab1.StatDbImpl]
StatDB.recover_wipe [lemma, in POCS.Lab1.StatDbImpl]
StatDB.statdb_abstraction [definition, in POCS.Lab1.StatDbImpl]
State [definition, in POCS.Lab1.StatDbAPI]
State [definition, in POCS.Common.OneDiskAPI]
State [record, in POCS.Common.NbdAPI]
State [record, in POCS.Lab1.VariablesAPI]
State [inductive, in POCS.Lab4.TwoDiskBaseAPI]
State [record, in POCS.Lab2.BadBlockAPI]
State [definition, in POCS.Lab3.LogAPI]
State [record, in POCS.Lab0.ThreeVariablesAPI]
stateBadBlock [projection, in POCS.Lab2.BadBlockAPI]
stateBadBlockInBounds [projection, in POCS.Lab2.BadBlockAPI]
StateCount [projection, in POCS.Lab1.VariablesAPI]
StateDisk [projection, in POCS.Common.NbdAPI]
stateDisk [projection, in POCS.Lab2.BadBlockAPI]
StateReq [projection, in POCS.Common.NbdAPI]
StateSum [projection, in POCS.Lab1.VariablesAPI]
StateVar [definition, in POCS.Lab0.ThreeVariablesAPI]
StateX [projection, in POCS.Lab0.ThreeVariablesAPI]
StateY [projection, in POCS.Lab0.ThreeVariablesAPI]
StateZ [projection, in POCS.Lab0.ThreeVariablesAPI]
step_fail1 [constructor, in POCS.Lab4.TwoDiskBaseAPI]
step_fail0 [constructor, in POCS.Lab4.TwoDiskBaseAPI]
step_id [constructor, in POCS.Lab4.TwoDiskBaseAPI]
step_size [constructor, in POCS.Lab4.TwoDiskBaseAPI]
step_write [constructor, in POCS.Lab4.TwoDiskBaseAPI]
step_read [constructor, in POCS.Lab4.TwoDiskBaseAPI]

T

td [module, in POCS.Lab4.ReplicatedServer]
then_init_compose [lemma, in POCS.Spec.Abstraction]
then_init [definition, in POCS.Spec.Abstraction]
ThreeVariablesAPI [library]
TwoDisk [module, in POCS.Lab4.TwoDiskImpl]
TwoDiskAPI [module, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI [library]
TwoDiskAPI.abstr [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.init [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.init_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read0_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read1_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.recover [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.recover_wipe [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size0_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size1_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write0_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write1_ok [axiom, in POCS.Lab4.TwoDiskAPI]
TwoDiskBase [module, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBaseAPI [module, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI [library]
TwoDiskBaseAPI.abstr [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.init [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.init_ok [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.read [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.read_ok [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.recover [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.recover_wipe [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.size [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.size_ok [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.write [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.write_ok [axiom, in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseImpl [library]
TwoDiskBase.abstr [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.init [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.init_ok [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.read [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.read_ok [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.recover [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.recover_wipe [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.size [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.size_ok [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.write [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.write_ok [axiom, in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskImpl [library]
TwoDisk.abstr [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.init [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.init_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.maybe_holds_stable [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.read [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.read0_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.read1_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.recover [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.recover_wipe [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.size [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.size0_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.size1_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.write [definition, in POCS.Lab4.TwoDiskImpl]
TwoDisk.write0_ok [lemma, in POCS.Lab4.TwoDiskImpl]
TwoDisk.write1_ok [lemma, in POCS.Lab4.TwoDiskImpl]
two_disks_are [definition, in POCS.Lab4.TwoDiskAPI]

U

UnknownOp [constructor, in POCS.Common.NbdAPI]

V

var [inductive, in POCS.Lab1.VariablesAPI]
var [inductive, in POCS.Lab0.ThreeVariablesAPI]
VarCount [constructor, in POCS.Lab1.VariablesAPI]
VariablesAPI [library]
VariablesImpl [library]
Vars [module, in POCS.Lab1.VariablesImpl]
VarsAPI [module, in POCS.Lab1.VariablesAPI]
VarsAPI [module, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.abstr [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.abstr [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.init [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.init [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.init_ok [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.init_ok [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.read [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.read [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.read_ok [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.read_ok [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.recover [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.recover [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.recover_wipe [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.recover_wipe [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.write [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.write [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.write_ok [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.write_ok [axiom, in POCS.Lab0.ThreeVariablesAPI]
VarSum [constructor, in POCS.Lab1.VariablesAPI]
Vars.abstr [axiom, in POCS.Lab1.VariablesImpl]
Vars.init [axiom, in POCS.Lab1.VariablesImpl]
Vars.init_ok [axiom, in POCS.Lab1.VariablesImpl]
Vars.read [axiom, in POCS.Lab1.VariablesImpl]
Vars.read_ok [axiom, in POCS.Lab1.VariablesImpl]
Vars.recover [axiom, in POCS.Lab1.VariablesImpl]
Vars.recover_wipe [axiom, in POCS.Lab1.VariablesImpl]
Vars.write [axiom, in POCS.Lab1.VariablesImpl]
Vars.write_ok [axiom, in POCS.Lab1.VariablesImpl]
VarX [constructor, in POCS.Lab0.ThreeVariablesAPI]
VarY [constructor, in POCS.Lab0.ThreeVariablesAPI]
VarZ [constructor, in POCS.Lab0.ThreeVariablesAPI]
var_eq [instance, in POCS.Lab0.ThreeVariablesAPI]

W

wipe_req [definition, in POCS.Common.NbdAPI]
Working [constructor, in POCS.Lab4.TwoDiskBaseAPI]
world [definition, in POCS.Spec.Proc]
world_crash [definition, in POCS.Spec.Proc]
Write [constructor, in POCS.Common.NbdAPI]
write_spec [definition, in POCS.Common.OneDiskAPI]
write_upd [definition, in POCS.Common.NbdAPI]
write_spec [definition, in POCS.Lab1.VariablesAPI]
write_spec [definition, in POCS.Lab2.BadBlockAPI]
write_spec [definition, in POCS.Lab0.ThreeVariablesAPI]
write0_spec [definition, in POCS.Lab4.TwoDiskAPI]
write1_spec [definition, in POCS.Lab4.TwoDiskAPI]

X

x [module, in POCS.Lab2.RemappedDiskImpl]

other

_ <- _ ; _ [notation, in POCS.Spec.Proc]
_ [ _ |=> _ ] [notation, in POCS.Lab3.LogImpl]
_ [ _ |-> _ ] [notation, in POCS.Lab3.LogImpl]
_ =??= _ [notation, in POCS.Helpers.Helpers]
_ =?= _ [notation, in POCS.Helpers.Helpers]
_ ?|= _ [notation, in POCS.Helpers.Helpers]
_ == _ [notation, in POCS.Helpers.Helpers]

Notation Index

other

_ <- _ ; _ [in POCS.Spec.Proc]
_ [ _ |=> _ ] [in POCS.Lab3.LogImpl]
_ [ _ |-> _ ] [in POCS.Lab3.LogImpl]
_ =??= _ [in POCS.Helpers.Helpers]
_ =?= _ [in POCS.Helpers.Helpers]
_ ?|= _ [in POCS.Helpers.Helpers]
_ == _ [in POCS.Helpers.Helpers]

Module Index

B

BadBlockAPI [in POCS.Lab2.BadBlockAPI]
BadBlockDisk [in POCS.Lab2.BadBlockImpl]
bad_disk [in POCS.Lab3.LogImpl]

D

d [in POCS.Lab2.RemappedServer]
DeexTests [in POCS.Helpers.Helpers]
DestructMatchesTests [in POCS.Helpers.Helpers]

E

Exercises [in POCS.Lab0.Exercises]

I

IO [in POCS.Spec.Proc]

L

log [in POCS.Lab3.LogImpl]
Log [in POCS.Lab3.LogImpl]
LogAPI [in POCS.Lab3.LogAPI]

N

nbd [in POCS.Common.NbdServer]
NbdAPI [in POCS.Common.NbdAPI]
NbdImpl [in POCS.Common.NbdImpl]
NBDServer [in POCS.Common.NbdServer]

O

OneDiskAPI [in POCS.Common.OneDiskAPI]

R

rd [in POCS.Lab4.ReplicatedServer]
RemappedDisk [in POCS.Lab2.RemappedDiskImpl]
remapped_disk [in POCS.Lab3.LogImpl]
ReplicatedDisk [in POCS.Lab4.ReplicatedDiskImpl]

S

s [in POCS.Lab4.ReplicatedServer]
s [in POCS.Lab2.RemappedServer]
SimplMatchTests [in POCS.Helpers.Helpers]
statdb [in POCS.Lab1.StatDbCli]
StatDB [in POCS.Lab1.StatDbImpl]
StatDbAPI [in POCS.Lab1.StatDbAPI]
StatDBImpl [in POCS.Lab1.StatDbImpl]

T

td [in POCS.Lab4.ReplicatedServer]
TwoDisk [in POCS.Lab4.TwoDiskImpl]
TwoDiskAPI [in POCS.Lab4.TwoDiskAPI]
TwoDiskBase [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBaseAPI [in POCS.Lab4.TwoDiskBaseAPI]

V

Vars [in POCS.Lab1.VariablesImpl]
VarsAPI [in POCS.Lab1.VariablesAPI]
VarsAPI [in POCS.Lab0.ThreeVariablesAPI]

X

x [in POCS.Lab2.RemappedDiskImpl]

Library Index

A

Abstraction

B

BadBlockAPI
BadBlockImpl

D

Disk

E

Exercises

H

Helpers

L

LogAPI
LogImpl

N

NbdAPI
NbdImpl
NbdServer

O

OneDiskAPI

P

POCS
Proc
ProcTheorems

R

Recovery
RemappedDiskImpl
RemappedServer
ReplicatedDiskImpl
ReplicatedServer

S

StatDbAPI
StatDbCli
StatDbImpl

T

ThreeVariablesAPI
TwoDiskAPI
TwoDiskBaseAPI
TwoDiskBaseImpl
TwoDiskImpl

V

VariablesAPI
VariablesImpl

Lemma Index

B

block0_block1_differ [in POCS.Helpers.Disk]

C

clos_refl_trans_1n_unit_tuple [in POCS.Spec.Recovery]
compose_recovery [in POCS.Spec.Recovery]

D

DeexTests.chooses_fresh_name [in POCS.Helpers.Helpers]
DeexTests.chooses_name [in POCS.Helpers.Helpers]
DestructMatchesTests.destructs_innermost_match [in POCS.Helpers.Helpers]
DestructMatchesTests.removes_absurdities [in POCS.Helpers.Helpers]
diskGets_app [in POCS.Helpers.Disk]
diskGets_last [in POCS.Helpers.Disk]
diskGets_first [in POCS.Helpers.Disk]
diskGet_eq_values [in POCS.Lab3.LogImpl]
diskShrink_diskUpd_notlast [in POCS.Helpers.Disk]
diskShrink_diskUpd_last [in POCS.Helpers.Disk]
diskShrink_preserves [in POCS.Helpers.Disk]
diskShrink_size [in POCS.Helpers.Disk]
diskUpds_diskGets_eq [in POCS.Helpers.Disk]
diskUpds_diskGets_neq [in POCS.Helpers.Disk]
diskUpds_diskUpd_before [in POCS.Helpers.Disk]
diskUpds_diskUpd_after [in POCS.Helpers.Disk]
diskUpds_diskUpd_comm [in POCS.Helpers.Disk]
diskUpds_size [in POCS.Helpers.Disk]
diskUpds_neq [in POCS.Helpers.Disk]
diskUpd_diskGets_neq [in POCS.Helpers.Disk]
diskUpd_oob_noop [in POCS.Helpers.Disk]
diskUpd_comm_lt [in POCS.Helpers.Disk]
diskUpd_comm [in POCS.Helpers.Disk]
diskUpd_twice [in POCS.Helpers.Disk]
diskUpd_same [in POCS.Helpers.Disk]
diskUpd_none [in POCS.Helpers.Disk]
diskUpd_neq [in POCS.Helpers.Disk]
diskUpd_oob_eq [in POCS.Helpers.Disk]
diskUpd_size [in POCS.Helpers.Disk]
diskUpd_eq [in POCS.Helpers.Disk]
diskUpd_eq_some [in POCS.Helpers.Disk]
disk_ext_inbounds_eq [in POCS.Helpers.Disk]
disk_ext_eq [in POCS.Helpers.Disk]
disk_oob_eq [in POCS.Helpers.Disk]
disk_none_oob [in POCS.Helpers.Disk]
disk_inbounds_not_none [in POCS.Helpers.Disk]
disk_inbounds_exists [in POCS.Helpers.Disk]

E

exec_recover_bind_inv [in POCS.Spec.ProcTheorems]
exec_ret [in POCS.Spec.ProcTheorems]
Exercises.addX_list_ok [in POCS.Lab0.Exercises]
Exercises.addX_ok [in POCS.Lab0.Exercises]
Exercises.add_odds_evens_ok_seems_good [in POCS.Lab0.Exercises]
Exercises.incX_ok_seems_good [in POCS.Lab0.Exercises]
Exercises.incX_ok [in POCS.Lab0.Exercises]
Exercises.incX_test [in POCS.Lab0.Exercises]
Exercises.swapXY_ok_seems_good [in POCS.Lab0.Exercises]
Exercises.swapXY_ok [in POCS.Lab0.Exercises]

H

holds_some_inv_eq [in POCS.Helpers.Helpers]
holds_in_some_eq [in POCS.Helpers.Helpers]
holds_in_some [in POCS.Helpers.Helpers]
holds_in_none_eq [in POCS.Helpers.Helpers]

I

idempotent_loopspec [in POCS.Spec.Recovery]
init_abstraction_any_rec [in POCS.Spec.Abstraction]

M

maybe_eq_list_map_some [in POCS.Helpers.Helpers]
maybe_eq_list_app [in POCS.Helpers.Helpers]
maybe_eq_list_last [in POCS.Helpers.Helpers]
maybe_eq_list_last_helper [in POCS.Helpers.Helpers]
maybe_eq_list_len [in POCS.Helpers.Helpers]
maybe_eq_list_first [in POCS.Helpers.Helpers]
maybe_eq_None_holds [in POCS.Helpers.Disk]
maybe_eq_None_is_True [in POCS.Helpers.Disk]
monad_assoc [in POCS.Spec.ProcTheorems]
monad_left_id [in POCS.Spec.ProcTheorems]

N

NBDServer.read_ok [in POCS.Common.NbdServer]
NBDServer.write_ok [in POCS.Common.NbdServer]

P

pred_missing [in POCS.Helpers.Helpers]
pred_weaken [in POCS.Helpers.Helpers]
proc_spec_rx [in POCS.Spec.Abstraction]
proc_spec_implication [in POCS.Spec.Abstraction]
proc_spec_weaken [in POCS.Spec.Abstraction]

R

rec_wipe_compose [in POCS.Spec.Recovery]
RemappedDisk.bad_block_inbounds [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover_wipe [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_noremap [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_remap [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write_ok [in POCS.Lab2.RemappedDiskImpl]
ReplicatedDisk.both_disks_not_missing [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.disks_eq_inbounds [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.diskUpd_maybe_same [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_size [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_0_to_eq [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after_diskUpd [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.exists_tuple2 [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.fixup_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.if_lt_dec [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_at_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init'_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.le_eq_or_S_le [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.missing0_implies_any [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.missing1_implies_any [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read_int_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_wipe [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_spec_idempotent [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_rok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_at_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.sizeInit_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size_int_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write_ok [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write_int_ok [in POCS.Lab4.ReplicatedDiskImpl]
ret_spec [in POCS.Spec.Abstraction]
rexec_finish_any_rec [in POCS.Spec.ProcTheorems]
rexec_equiv [in POCS.Spec.ProcTheorems]

S

SimplMatchTests.fails_on_hyp_if_match_not_removed [in POCS.Helpers.Helpers]
SimplMatchTests.fails_if_match_not_removed [in POCS.Helpers.Helpers]
SimplMatchTests.removes_match [in POCS.Helpers.Helpers]
spec_abstraction_compose [in POCS.Spec.Abstraction]
spec_exec_equiv [in POCS.Spec.Abstraction]
spec_intros [in POCS.Spec.Abstraction]
StatDB.add_ok [in POCS.Lab1.StatDbImpl]
StatDB.init_ok [in POCS.Lab1.StatDbImpl]
StatDB.mean_ok [in POCS.Lab1.StatDbImpl]
StatDB.recover_wipe [in POCS.Lab1.StatDbImpl]

T

then_init_compose [in POCS.Spec.Abstraction]
TwoDisk.init_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.maybe_holds_stable [in POCS.Lab4.TwoDiskImpl]
TwoDisk.read0_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.read1_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.recover_wipe [in POCS.Lab4.TwoDiskImpl]
TwoDisk.size0_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.size1_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.write0_ok [in POCS.Lab4.TwoDiskImpl]
TwoDisk.write1_ok [in POCS.Lab4.TwoDiskImpl]

Constructor Index

B

BaseOp [in POCS.Spec.Proc]
Bind [in POCS.Spec.Proc]
BothDisks [in POCS.Lab4.TwoDiskBaseAPI]

C

Crashed [in POCS.Spec.Proc]

D

Disconnect [in POCS.Common.NbdAPI]
d0 [in POCS.Lab4.TwoDiskBaseAPI]
d1 [in POCS.Lab4.TwoDiskBaseAPI]

E

EInvalid [in POCS.Common.NbdAPI]
ENospc [in POCS.Common.NbdAPI]
equal_dec [in POCS.Helpers.Helpers]
ESuccess [in POCS.Common.NbdAPI]
ExecBindCrashed [in POCS.Spec.Proc]
ExecBindFinished [in POCS.Spec.Proc]
ExecCrashBegin [in POCS.Spec.Proc]
ExecCrashEnd [in POCS.Spec.Proc]
ExecOp [in POCS.Spec.Proc]
ExecRecoverCrashDuringRecovery [in POCS.Spec.Proc]
ExecRecoverExec [in POCS.Spec.Proc]
ExecRet [in POCS.Spec.Proc]

F

Failed [in POCS.Lab4.TwoDiskBaseAPI]
Finished [in POCS.Spec.Proc]
Flush [in POCS.Common.NbdAPI]

I

InitFailed [in POCS.Spec.Abstraction]
Initialized [in POCS.Spec.Abstraction]

M

mark [in POCS.Spec.Abstraction]
mkState [in POCS.Common.NbdAPI]
mkState [in POCS.Lab1.VariablesAPI]
mkState [in POCS.Lab2.BadBlockAPI]
mkState [in POCS.Lab0.ThreeVariablesAPI]

O

OnlyDisk0 [in POCS.Lab4.TwoDiskBaseAPI]
OnlyDisk1 [in POCS.Lab4.TwoDiskBaseAPI]
op_size [in POCS.Lab4.TwoDiskBaseAPI]
op_write [in POCS.Lab4.TwoDiskBaseAPI]
op_read [in POCS.Lab4.TwoDiskBaseAPI]

R

Read [in POCS.Common.NbdAPI]
Recovered [in POCS.Spec.Proc]
RemappedDisk.RemappedAbstraction [in POCS.Lab2.RemappedDiskImpl]
ReplicatedDisk.Continue [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.FullySynced [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.OutOfSync [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.RepairDoneOrFailed [in POCS.Lab4.ReplicatedDiskImpl]
Ret [in POCS.Spec.Proc]
RExec [in POCS.Spec.Proc]
RExecCrash [in POCS.Spec.Proc]
RFinished [in POCS.Spec.Proc]

S

Spec [in POCS.Spec.Abstraction]
step_fail1 [in POCS.Lab4.TwoDiskBaseAPI]
step_fail0 [in POCS.Lab4.TwoDiskBaseAPI]
step_id [in POCS.Lab4.TwoDiskBaseAPI]
step_size [in POCS.Lab4.TwoDiskBaseAPI]
step_write [in POCS.Lab4.TwoDiskBaseAPI]
step_read [in POCS.Lab4.TwoDiskBaseAPI]

U

UnknownOp [in POCS.Common.NbdAPI]

V

VarCount [in POCS.Lab1.VariablesAPI]
VarSum [in POCS.Lab1.VariablesAPI]
VarX [in POCS.Lab0.ThreeVariablesAPI]
VarY [in POCS.Lab0.ThreeVariablesAPI]
VarZ [in POCS.Lab0.ThreeVariablesAPI]

W

Working [in POCS.Lab4.TwoDiskBaseAPI]
Write [in POCS.Common.NbdAPI]

Axiom Index

A

addr_to_block_ok [in POCS.Lab3.LogImpl]
addr_to_block [in POCS.Lab3.LogImpl]

B

BadBlockAPI.abstr [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover_wipe [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write_ok [in POCS.Lab2.BadBlockAPI]
BadBlockDisk.abstr [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover_wipe [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write_ok [in POCS.Lab2.BadBlockImpl]
bappend [in POCS.Helpers.Disk]
baseModel [in POCS.Spec.Proc]
block_to_addr [in POCS.Lab3.LogImpl]
bsplit [in POCS.Helpers.Disk]
bsplit_bappend [in POCS.Helpers.Disk]
bytes [in POCS.Helpers.Disk]
bytes_differ [in POCS.Helpers.Disk]
bytes_dec [in POCS.Helpers.Disk]
bytes0 [in POCS.Helpers.Disk]
bytes1 [in POCS.Helpers.Disk]

G

get_new_item [in POCS.Lab1.StatDbCli]

H

Handle [in POCS.Common.NbdAPI]

L

LogAPI.abstr [in POCS.Lab3.LogAPI]
LogAPI.append [in POCS.Lab3.LogAPI]
LogAPI.append_ok [in POCS.Lab3.LogAPI]
LogAPI.get [in POCS.Lab3.LogAPI]
LogAPI.get_ok [in POCS.Lab3.LogAPI]
LogAPI.init [in POCS.Lab3.LogAPI]
LogAPI.init_ok [in POCS.Lab3.LogAPI]
LogAPI.recover [in POCS.Lab3.LogAPI]
LogAPI.recover_wipe [in POCS.Lab3.LogAPI]
LogAPI.reset [in POCS.Lab3.LogAPI]
LogAPI.reset_ok [in POCS.Lab3.LogAPI]
Log.abstr [in POCS.Lab3.LogImpl]
Log.append_ok [in POCS.Lab3.LogImpl]
Log.get_ok [in POCS.Lab3.LogImpl]
Log.init_ok [in POCS.Lab3.LogImpl]
Log.recover_wipe [in POCS.Lab3.LogImpl]
Log.reset_ok [in POCS.Lab3.LogImpl]

N

NbdAPI.abstr [in POCS.Common.NbdAPI]
NbdAPI.getRequest [in POCS.Common.NbdAPI]
NbdAPI.getRequest_ok [in POCS.Common.NbdAPI]
NbdAPI.init [in POCS.Common.NbdAPI]
NbdAPI.init_ok [in POCS.Common.NbdAPI]
NbdAPI.recover [in POCS.Common.NbdAPI]
NbdAPI.recover_wipe [in POCS.Common.NbdAPI]
NbdAPI.sendResponse [in POCS.Common.NbdAPI]
NbdAPI.sendResponse_ok [in POCS.Common.NbdAPI]
NbdImpl.abstr [in POCS.Common.NbdImpl]
NbdImpl.getRequest [in POCS.Common.NbdImpl]
NbdImpl.getRequest_ok [in POCS.Common.NbdImpl]
NbdImpl.init [in POCS.Common.NbdImpl]
NbdImpl.init_ok [in POCS.Common.NbdImpl]
NbdImpl.recover [in POCS.Common.NbdImpl]
NbdImpl.recover_wipe [in POCS.Common.NbdImpl]
NbdImpl.sendResponse [in POCS.Common.NbdImpl]
NbdImpl.sendResponse_ok [in POCS.Common.NbdImpl]

O

OneDiskAPI.abstr [in POCS.Common.OneDiskAPI]
OneDiskAPI.init [in POCS.Common.OneDiskAPI]
OneDiskAPI.init_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.read [in POCS.Common.OneDiskAPI]
OneDiskAPI.read_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.recover [in POCS.Common.OneDiskAPI]
OneDiskAPI.recover_wipe [in POCS.Common.OneDiskAPI]
OneDiskAPI.size [in POCS.Common.OneDiskAPI]
OneDiskAPI.size_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.write [in POCS.Common.OneDiskAPI]
OneDiskAPI.write_ok [in POCS.Common.OneDiskAPI]

R

report_mean [in POCS.Lab1.StatDbCli]

S

StatDbAPI.abstr [in POCS.Lab1.StatDbAPI]
StatDbAPI.add [in POCS.Lab1.StatDbAPI]
StatDbAPI.add_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.init [in POCS.Lab1.StatDbAPI]
StatDbAPI.init_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.mean [in POCS.Lab1.StatDbAPI]
StatDbAPI.mean_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.recover [in POCS.Lab1.StatDbAPI]
StatDbAPI.recover_wipe [in POCS.Lab1.StatDbAPI]

T

TwoDiskAPI.abstr [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.init [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.init_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read0_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.read1_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.recover [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.recover_wipe [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size0_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.size1_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write0_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskAPI.write1_ok [in POCS.Lab4.TwoDiskAPI]
TwoDiskBaseAPI.abstr [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.init [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.init_ok [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.read [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.read_ok [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.recover [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.recover_wipe [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.size [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.size_ok [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.write [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBaseAPI.write_ok [in POCS.Lab4.TwoDiskBaseAPI]
TwoDiskBase.abstr [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.init [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.init_ok [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.read [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.read_ok [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.recover [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.recover_wipe [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.size [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.size_ok [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.write [in POCS.Lab4.TwoDiskBaseImpl]
TwoDiskBase.write_ok [in POCS.Lab4.TwoDiskBaseImpl]

V

VarsAPI.abstr [in POCS.Lab1.VariablesAPI]
VarsAPI.abstr [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.init [in POCS.Lab1.VariablesAPI]
VarsAPI.init [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.init_ok [in POCS.Lab1.VariablesAPI]
VarsAPI.init_ok [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.read [in POCS.Lab1.VariablesAPI]
VarsAPI.read [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.read_ok [in POCS.Lab1.VariablesAPI]
VarsAPI.read_ok [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.recover [in POCS.Lab1.VariablesAPI]
VarsAPI.recover [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.recover_wipe [in POCS.Lab1.VariablesAPI]
VarsAPI.recover_wipe [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.write [in POCS.Lab1.VariablesAPI]
VarsAPI.write [in POCS.Lab0.ThreeVariablesAPI]
VarsAPI.write_ok [in POCS.Lab1.VariablesAPI]
VarsAPI.write_ok [in POCS.Lab0.ThreeVariablesAPI]
Vars.abstr [in POCS.Lab1.VariablesImpl]
Vars.init [in POCS.Lab1.VariablesImpl]
Vars.init_ok [in POCS.Lab1.VariablesImpl]
Vars.read [in POCS.Lab1.VariablesImpl]
Vars.read_ok [in POCS.Lab1.VariablesImpl]
Vars.recover [in POCS.Lab1.VariablesImpl]
Vars.recover_wipe [in POCS.Lab1.VariablesImpl]
Vars.write [in POCS.Lab1.VariablesImpl]
Vars.write_ok [in POCS.Lab1.VariablesImpl]

Inductive Index

B

bg_failure [in POCS.Lab4.TwoDiskBaseAPI]

D

diskId [in POCS.Lab4.TwoDiskBaseAPI]
DiskResult [in POCS.Lab4.TwoDiskBaseAPI]

E

EqualDec [in POCS.Helpers.Helpers]
ErrorCode [in POCS.Common.NbdAPI]
exec [in POCS.Spec.Proc]
exec_recover [in POCS.Spec.Proc]

I

InitResult [in POCS.Spec.Abstraction]

M

Marker [in POCS.Spec.Abstraction]

O

Op [in POCS.Lab4.TwoDiskBaseAPI]
op_step [in POCS.Lab4.TwoDiskBaseAPI]

P

proc [in POCS.Spec.Proc]

R

RemappedDisk.remapped_abstraction [in POCS.Lab2.RemappedDiskImpl]
ReplicatedDisk.DiskStatus [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.RecStatus [in POCS.Lab4.ReplicatedDiskImpl]
Request [in POCS.Common.NbdAPI]
Result [in POCS.Spec.Proc]
rexec [in POCS.Spec.Proc]
RResult [in POCS.Spec.Proc]

S

State [in POCS.Lab4.TwoDiskBaseAPI]

V

var [in POCS.Lab1.VariablesAPI]
var [in POCS.Lab0.ThreeVariablesAPI]

Projection Index

A

abstraction [in POCS.Spec.Abstraction]

D

data [in POCS.Common.NbdAPI]
data_len [in POCS.Common.NbdAPI]

E

equal_dec [in POCS.Helpers.Helpers]
error [in POCS.Common.NbdAPI]

I

IO.baseOpT [in POCS.Spec.Proc]
IO.base_step [in POCS.Spec.Proc]
IO.world [in POCS.Spec.Proc]
IO.world_crash [in POCS.Spec.Proc]

P

post [in POCS.Spec.Abstraction]
pre [in POCS.Spec.Abstraction]

R

recovered [in POCS.Spec.Abstraction]
rhandle [in POCS.Common.NbdAPI]

S

stateBadBlock [in POCS.Lab2.BadBlockAPI]
stateBadBlockInBounds [in POCS.Lab2.BadBlockAPI]
StateCount [in POCS.Lab1.VariablesAPI]
StateDisk [in POCS.Common.NbdAPI]
stateDisk [in POCS.Lab2.BadBlockAPI]
StateReq [in POCS.Common.NbdAPI]
StateSum [in POCS.Lab1.VariablesAPI]
StateX [in POCS.Lab0.ThreeVariablesAPI]
StateY [in POCS.Lab0.ThreeVariablesAPI]
StateZ [in POCS.Lab0.ThreeVariablesAPI]

Instance Index

B

bool_equal_dec [in POCS.Helpers.Helpers]

E

exec_equiv_equiv [in POCS.Spec.ProcTheorems]

N

nat_equal_dec [in POCS.Helpers.Helpers]

V

var_eq [in POCS.Lab0.ThreeVariablesAPI]

Definition Index

A

Abstraction [in POCS.Spec.Abstraction]
abstraction_compose [in POCS.Spec.Abstraction]
addr [in POCS.Helpers.Disk]
addr_to_block_spec [in POCS.Lab3.LogImpl]
add_spec [in POCS.Lab1.StatDbAPI]
append_spec [in POCS.Lab3.LogAPI]

B

baseOpT [in POCS.Spec.Proc]
base_step [in POCS.Spec.Proc]
block [in POCS.Helpers.Disk]
blockbytes [in POCS.Helpers.Disk]
block0 [in POCS.Helpers.Disk]
block1 [in POCS.Helpers.Disk]
bnull [in POCS.Helpers.Disk]
bsplit_list [in POCS.Helpers.Disk]

C

cli [in POCS.Lab1.StatDbCli]
combined_step [in POCS.Lab4.TwoDiskBaseAPI]

D

disk [in POCS.Helpers.Disk]
diskGet [in POCS.Helpers.Disk]
diskGets [in POCS.Helpers.Disk]
diskShrink [in POCS.Helpers.Disk]
diskSize [in POCS.Helpers.Disk]
diskUpd [in POCS.Helpers.Disk]
diskUpds [in POCS.Helpers.Disk]
disk0 [in POCS.Lab4.TwoDiskBaseAPI]
disk1 [in POCS.Lab4.TwoDiskBaseAPI]

E

empty_disk [in POCS.Helpers.Disk]
exec_equiv [in POCS.Spec.ProcTheorems]
Exercises.addX [in POCS.Lab0.Exercises]
Exercises.addX_list [in POCS.Lab0.Exercises]
Exercises.add_odds_evens [in POCS.Lab0.Exercises]
Exercises.incX [in POCS.Lab0.Exercises]
Exercises.list_sum [in POCS.Lab0.Exercises]
Exercises.swapXY [in POCS.Lab0.Exercises]

G

getBadBlock_spec [in POCS.Lab2.BadBlockAPI]
getRequest_spec [in POCS.Common.NbdAPI]
get_disk [in POCS.Lab4.TwoDiskBaseAPI]
get_spec [in POCS.Lab3.LogAPI]

I

IdAbstraction [in POCS.Spec.Abstraction]
idempotent [in POCS.Spec.Recovery]
init [in POCS.Lab4.ReplicatedServer]
init [in POCS.Lab2.RemappedServer]
inited [in POCS.Lab1.StatDbAPI]
inited [in POCS.Common.NbdAPI]
inited_any [in POCS.Spec.Abstraction]
init_abstraction [in POCS.Spec.Abstraction]

L

Log.append [in POCS.Lab3.LogImpl]
Log.get [in POCS.Lab3.LogImpl]
Log.init [in POCS.Lab3.LogImpl]
Log.recover [in POCS.Lab3.LogImpl]
Log.reset [in POCS.Lab3.LogImpl]
loop [in POCS.Lab1.StatDbCli]

M

maybe_eq_list [in POCS.Helpers.Helpers]
maybe_eq [in POCS.Helpers.Helpers]
maybe_holds [in POCS.Helpers.Helpers]
mean_spec [in POCS.Lab1.StatDbAPI]
missing [in POCS.Helpers.Helpers]

N

NBDServer.handle [in POCS.Common.NbdServer]
NBDServer.init [in POCS.Common.NbdServer]
NBDServer.read [in POCS.Common.NbdServer]
NBDServer.serverLoop [in POCS.Common.NbdServer]
NBDServer.size [in POCS.Common.NbdServer]
NBDServer.write [in POCS.Common.NbdServer]
no_crash [in POCS.Spec.Recovery]
no_wipe [in POCS.Spec.Recovery]

O

op_spec [in POCS.Spec.Recovery]

P

post_step [in POCS.Spec.Recovery]
pre_step [in POCS.Spec.Recovery]
proc_loopspec [in POCS.Spec.Recovery]
proc_spec [in POCS.Spec.Abstraction]

R

read_spec [in POCS.Common.OneDiskAPI]
read_match' [in POCS.Common.NbdAPI]
read_match [in POCS.Common.NbdAPI]
read_spec [in POCS.Lab1.VariablesAPI]
read_spec [in POCS.Lab2.BadBlockAPI]
read_spec [in POCS.Lab0.ThreeVariablesAPI]
read0_spec [in POCS.Lab4.TwoDiskAPI]
read1_spec [in POCS.Lab4.TwoDiskAPI]
rec_wipe [in POCS.Spec.Abstraction]
RemappedDisk.abstr [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_5_nok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_4_nok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_3_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_2_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_1_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init' [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write [in POCS.Lab2.RemappedDiskImpl]
ReplicatedDisk.abstr [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.equal_after [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.fixup [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init_at [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.init' [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.rd_abstraction [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.read [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.Recover_spec [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.recover_at [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.size [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.sizeInit [in POCS.Lab4.ReplicatedDiskImpl]
ReplicatedDisk.write [in POCS.Lab4.ReplicatedDiskImpl]
reset_spec [in POCS.Lab3.LogAPI]

S

Semantics [in POCS.Spec.Recovery]
sendResponse_spec [in POCS.Common.NbdAPI]
serverLoop [in POCS.Lab4.ReplicatedServer]
serverLoop [in POCS.Lab2.RemappedServer]
set_disk [in POCS.Lab4.TwoDiskBaseAPI]
size [in POCS.Lab4.ReplicatedServer]
size [in POCS.Lab2.RemappedServer]
size_spec [in POCS.Common.OneDiskAPI]
size_spec [in POCS.Lab2.BadBlockAPI]
size0_spec [in POCS.Lab4.TwoDiskAPI]
size1_spec [in POCS.Lab4.TwoDiskAPI]
Specification [in POCS.Spec.Abstraction]
spec_impl [in POCS.Spec.Abstraction]
StatDB.abstr [in POCS.Lab1.StatDbImpl]
StatDB.abstr_5_nok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_4_nok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_3_ok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_2_ok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_1_ok [in POCS.Lab1.StatDbImpl]
StatDB.add [in POCS.Lab1.StatDbImpl]
StatDB.init [in POCS.Lab1.StatDbImpl]
StatDB.init' [in POCS.Lab1.StatDbImpl]
StatDB.mean [in POCS.Lab1.StatDbImpl]
StatDB.recover [in POCS.Lab1.StatDbImpl]
StatDB.statdb_abstraction [in POCS.Lab1.StatDbImpl]
State [in POCS.Lab1.StatDbAPI]
State [in POCS.Common.OneDiskAPI]
State [in POCS.Lab3.LogAPI]
StateVar [in POCS.Lab0.ThreeVariablesAPI]

T

then_init [in POCS.Spec.Abstraction]
TwoDisk.abstr [in POCS.Lab4.TwoDiskImpl]
TwoDisk.init [in POCS.Lab4.TwoDiskImpl]
TwoDisk.read [in POCS.Lab4.TwoDiskImpl]
TwoDisk.recover [in POCS.Lab4.TwoDiskImpl]
TwoDisk.size [in POCS.Lab4.TwoDiskImpl]
TwoDisk.write [in POCS.Lab4.TwoDiskImpl]
two_disks_are [in POCS.Lab4.TwoDiskAPI]

W

wipe_req [in POCS.Common.NbdAPI]
world [in POCS.Spec.Proc]
world_crash [in POCS.Spec.Proc]
write_spec [in POCS.Common.OneDiskAPI]
write_upd [in POCS.Common.NbdAPI]
write_spec [in POCS.Lab1.VariablesAPI]
write_spec [in POCS.Lab2.BadBlockAPI]
write_spec [in POCS.Lab0.ThreeVariablesAPI]
write0_spec [in POCS.Lab4.TwoDiskAPI]
write1_spec [in POCS.Lab4.TwoDiskAPI]

Record Index

E

EqualDec [in POCS.Helpers.Helpers]

I

IO.Model [in POCS.Spec.Proc]

L

LayerAbstraction [in POCS.Spec.Abstraction]

R

Response [in POCS.Common.NbdAPI]

S

SpecProps [in POCS.Spec.Abstraction]
State [in POCS.Common.NbdAPI]
State [in POCS.Lab1.VariablesAPI]
State [in POCS.Lab2.BadBlockAPI]
State [in POCS.Lab0.ThreeVariablesAPI]

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(635 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(36 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(30 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(132 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(60 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(159 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(22 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(23 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(153 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)