Global Index

Z

_

(1466 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

_

(6 entries)

Binder Index

T

W

Z

_

(1148 entries)

Library Index

B

D

G

J

K

L

N

O

P

Q

U

V

W

X

Y

Z

_

other

(25 entries)

Lemma Index

A

F

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(39 entries)

Constructor Index

B

F

H

J

K

N

O

Q

U

V

X

Y

Z

_

other

(44 entries)

Axiom Index

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

Inductive Index

A

B

F

G

J

K

L

P

Q

T

U

W

X

Y

Z

_

other

(26 entries)

Projection Index

B

E

F

G

H

J

K

L

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(12 entries)

Instance Index

A

B

G

J

K

L

N

O

Q

U

V

W

X

Y

Z

_

other

(56 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

J

K

L

P

Q

X

Y

Z

_

(83 entries)

Record Index

A

B

E

F

G

I

J

K

L

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

Global Index

A

address [axiom, in FreeSpec.Example.smram]
address_eq_dec [axiom, in FreeSpec.Example.smram]
address_eq_refl [axiom, in FreeSpec.Example.smram]
address_eq [axiom, in FreeSpec.Example.smram]
addr':12 [binder, in FreeSpec.Example.smram]
addr':5 [binder, in FreeSpec.Example.smram]
addr':8 [binder, in FreeSpec.Example.smram]
addr':85 [binder, in FreeSpec.Example.smram]
addr:11 [binder, in FreeSpec.Example.smram]
addr:111 [binder, in FreeSpec.Example.smram]
addr:115 [binder, in FreeSpec.Example.smram]
addr:16 [binder, in FreeSpec.Example.smram]
addr:17 [binder, in FreeSpec.Example.smram]
addr:26 [binder, in FreeSpec.Example.smram]
addr:30 [binder, in FreeSpec.Example.smram]
addr:39 [binder, in FreeSpec.Example.smram]
addr:4 [binder, in FreeSpec.Example.smram]
addr:43 [binder, in FreeSpec.Example.smram]
addr:50 [binder, in FreeSpec.Example.smram]
addr:52 [binder, in FreeSpec.Example.smram]
addr:66 [binder, in FreeSpec.Example.smram]
addr:7 [binder, in FreeSpec.Example.smram]
addr:83 [binder, in FreeSpec.Example.smram]
airlock [library]
Assign [constructor, in FreeSpec.FFI.Refs]
assign [projection, in FreeSpec.FFI.Refs]
a:1 [binder, in FreeSpec.Exec.Eval]
a:1 [binder, in FreeSpec.FFI.Refs]
a:101 [binder, in FreeSpec.Example.smram]
a:103 [binder, in FreeSpec.Example.airlock]
a:105 [binder, in FreeSpec.Example.smram]
a:107 [binder, in FreeSpec.Core.SemanticsFacts]
a:11 [binder, in FreeSpec.FFI.Refs]
a:111 [binder, in FreeSpec.Core.SemanticsFacts]
a:117 [binder, in FreeSpec.Core.SemanticsFacts]
a:120 [binder, in FreeSpec.Example.smram]
a:123 [binder, in FreeSpec.Core.SemanticsFacts]
a:129 [binder, in FreeSpec.Core.SemanticsFacts]
a:13 [binder, in FreeSpec.FFI.Refs]
a:135 [binder, in FreeSpec.Example.smram]
a:135 [binder, in FreeSpec.Core.SemanticsFacts]
a:141 [binder, in FreeSpec.Core.SemanticsFacts]
a:147 [binder, in FreeSpec.Core.SemanticsFacts]
a:149 [binder, in FreeSpec.Core.SemanticsFacts]
a:15 [binder, in FreeSpec.FFI.Refs]
a:15 [binder, in FreeSpec.Core.InstrumentFacts]
a:151 [binder, in FreeSpec.Core.SemanticsFacts]
a:153 [binder, in FreeSpec.Core.SemanticsFacts]
a:18 [binder, in FreeSpec.Core.Instrument]
a:19 [binder, in FreeSpec.FFI.Refs]
a:20 [binder, in FreeSpec.FFI.Refs]
a:21 [binder, in FreeSpec.Example.smram]
a:21 [binder, in FreeSpec.FFI.Refs]
a:24 [binder, in FreeSpec.FFI.Refs]
a:24 [binder, in FreeSpec.Core.InstrumentFacts]
a:28 [binder, in FreeSpec.FFI.Refs]
a:30 [binder, in FreeSpec.Core.HoareFacts]
a:317 [binder, in FreeSpec.Core.Interface]
a:32 [binder, in FreeSpec.FFI.Refs]
a:330 [binder, in FreeSpec.Core.Interface]
a:34 [binder, in FreeSpec.Example.smram]
a:34 [binder, in FreeSpec.Core.InstrumentFacts]
a:38 [binder, in FreeSpec.Core.ImpureFacts]
a:4 [binder, in FreeSpec.Core.Init]
a:42 [binder, in FreeSpec.Core.HoareFacts]
a:44 [binder, in FreeSpec.Core.Semantics]
a:45 [binder, in FreeSpec.Core.Hoare]
a:49 [binder, in FreeSpec.Core.Semantics]
a:5 [binder, in FreeSpec.FFI.Refs]
a:50 [binder, in FreeSpec.Core.SemanticsFacts]
a:51 [binder, in FreeSpec.Core.Impure]
a:53 [binder, in FreeSpec.Core.Semantics]
a:53 [binder, in FreeSpec.Core.SemanticsFacts]
A:54 [binder, in FreeSpec.Example.smram]
a:55 [binder, in FreeSpec.Example.airlock]
a:57 [binder, in FreeSpec.Core.Semantics]
a:57 [binder, in FreeSpec.Example.smram]
a:58 [binder, in FreeSpec.Core.HoareFacts]
a:59 [binder, in FreeSpec.Example.airlock]
a:6 [binder, in FreeSpec.Core.ComponentFacts]
a:6 [binder, in FreeSpec.Core.Instrument]
a:6 [binder, in FreeSpec.Core.InstrumentFacts]
a:67 [binder, in FreeSpec.Example.airlock]
a:7 [binder, in FreeSpec.FFI.Refs]
a:7 [binder, in FreeSpec.Core.Init]
a:72 [binder, in FreeSpec.Core.Semantics]
a:79 [binder, in FreeSpec.Core.HoareFacts]
a:8 [binder, in FreeSpec.Exec.Eval]
a:87 [binder, in FreeSpec.Example.smram]
a:9 [binder, in FreeSpec.Core.Component]
a:9 [binder, in FreeSpec.FFI.Refs]
a:91 [binder, in FreeSpec.Example.smram]
a:94 [binder, in FreeSpec.Example.smram]
a:97 [binder, in FreeSpec.Example.smram]

B

bind_request_then_assoc [lemma, in FreeSpec.Core.ImpureFacts]
bootstrap [definition, in FreeSpec.Core.Component]
b:112 [binder, in FreeSpec.Core.SemanticsFacts]
b:117 [binder, in FreeSpec.Example.smram]
b:118 [binder, in FreeSpec.Core.SemanticsFacts]
b:124 [binder, in FreeSpec.Core.SemanticsFacts]
b:13 [binder, in FreeSpec.Core.Init]
b:130 [binder, in FreeSpec.Core.SemanticsFacts]
b:136 [binder, in FreeSpec.Core.SemanticsFacts]
b:142 [binder, in FreeSpec.Core.SemanticsFacts]
b:40 [binder, in FreeSpec.Core.ImpureFacts]
b:46 [binder, in FreeSpec.Core.HoareFacts]
B:55 [binder, in FreeSpec.Example.smram]
b:60 [binder, in FreeSpec.Core.HoareFacts]
b:8 [binder, in FreeSpec.Core.Init]

C

callee_obligation [projection, in FreeSpec.Core.Contract]
caller_obligation [projection, in FreeSpec.Core.Contract]
cell [axiom, in FreeSpec.Example.smram]
ci:18 [binder, in FreeSpec.Core.ComponentFacts]
ci:37 [binder, in FreeSpec.Core.ComponentFacts]
ci:75 [binder, in FreeSpec.Core.Contract]
ci:76 [binder, in FreeSpec.Core.HoareFacts]
cj:20 [binder, in FreeSpec.Core.ComponentFacts]
cj:39 [binder, in FreeSpec.Core.ComponentFacts]
cj:76 [binder, in FreeSpec.Core.Contract]
cj:78 [binder, in FreeSpec.Core.HoareFacts]
close_door_run [lemma, in FreeSpec.Example.airlock]
close_door_respectful [lemma, in FreeSpec.Example.airlock]
close_door [definition, in FreeSpec.Example.airlock]
co [definition, in FreeSpec.Example.airlock]
compliant_semantics_Proper [instance, in FreeSpec.Core.SemanticsFacts]
compliant_semantics_caller_obligation_compliant [lemma, in FreeSpec.Core.SemanticsFacts]
compliant_semantics_caller_obligation_callee_obligation [lemma, in FreeSpec.Core.SemanticsFacts]
compliant_semantics_rec [constructor, in FreeSpec.Core.SemanticsFacts]
compliant_semantics [inductive, in FreeSpec.Core.SemanticsFacts]
component [definition, in FreeSpec.Core.Component]
Component [library]
ComponentFacts [library]
comp:154 [binder, in FreeSpec.Example.smram]
comp:28 [binder, in FreeSpec.Core.SemanticsFacts]
comp:28 [binder, in FreeSpec.Core.InstrumentFacts]
comp:38 [binder, in FreeSpec.Core.InstrumentFacts]
comp:39 [binder, in FreeSpec.Core.SemanticsFacts]
comp:46 [binder, in FreeSpec.Core.ComponentFacts]
cond:3 [binder, in FreeSpec.Core.Init]
const_witness [definition, in FreeSpec.Core.Contract]
content:112 [binder, in FreeSpec.Example.smram]
content:116 [binder, in FreeSpec.Example.smram]
content:84 [binder, in FreeSpec.Example.smram]
contract [record, in FreeSpec.Core.Contract]
Contract [library]
contractprod [definition, in FreeSpec.Core.Contract]
controller [definition, in FreeSpec.Example.airlock]
CONTROLLER [inductive, in FreeSpec.Example.airlock]
controller_correct [lemma, in FreeSpec.Example.airlock]
Core [library]
CoreFacts [library]
correct_component_derives_compliant_semantics [lemma, in FreeSpec.Core.ComponentFacts]
correct_component [definition, in FreeSpec.Core.ComponentFacts]
correct:41 [binder, in FreeSpec.Core.ComponentFacts]
cpt:44 [binder, in FreeSpec.Example.airlock]
c:10 [binder, in FreeSpec.Core.ComponentFacts]
c:105 [binder, in FreeSpec.Core.SemanticsFacts]
c:14 [binder, in FreeSpec.Core.Instrument]
c:14 [binder, in FreeSpec.Core.Component]
c:14 [binder, in FreeSpec.Core.InstrumentFacts]
c:16 [binder, in FreeSpec.Core.ComponentFacts]
c:18 [binder, in FreeSpec.Core.Component]
c:22 [binder, in FreeSpec.Core.SemanticsFacts]
c:23 [binder, in FreeSpec.Core.InstrumentFacts]
c:28 [binder, in FreeSpec.Core.Component]
c:29 [binder, in FreeSpec.Core.HoareFacts]
c:3 [binder, in FreeSpec.Core.ComponentFacts]
c:33 [binder, in FreeSpec.Core.InstrumentFacts]
c:34 [binder, in FreeSpec.Core.SemanticsFacts]
c:35 [binder, in FreeSpec.Core.ComponentFacts]
c:41 [binder, in FreeSpec.Core.HoareFacts]
c:42 [binder, in FreeSpec.Core.ImpureFacts]
c:44 [binder, in FreeSpec.Core.Hoare]
c:45 [binder, in FreeSpec.Core.Contract]
c:5 [binder, in FreeSpec.Core.Instrument]
c:5 [binder, in FreeSpec.Core.SemanticsFacts]
c:5 [binder, in FreeSpec.Core.InstrumentFacts]
c:54 [binder, in FreeSpec.Core.Contract]
c:55 [binder, in FreeSpec.Core.Hoare]
c:57 [binder, in FreeSpec.Core.HoareFacts]
c:6 [binder, in FreeSpec.Core.Component]
c:62 [binder, in FreeSpec.Core.Contract]

D

default_MayProvide [instance, in FreeSpec.Core.Interface]
Deref [constructor, in FreeSpec.FFI.Refs]
deref [projection, in FreeSpec.FFI.Refs]
derive_semantics_equ [lemma, in FreeSpec.Core.ComponentFacts]
derive_semantics' [definition, in FreeSpec.Core.ComponentFacts]
derive_semantics [definition, in FreeSpec.Core.Component]
dispatch [definition, in FreeSpec.Example.smram]
distinguish [projection, in FreeSpec.Core.Interface]
Distinguish [record, in FreeSpec.Core.Interface]
Distinguish0:138 [binder, in FreeSpec.Core.Interface]
Distinguish0:148 [binder, in FreeSpec.Core.Interface]
Distinguish0:160 [binder, in FreeSpec.Core.Interface]
Distinguish0:177 [binder, in FreeSpec.Core.Interface]
Distinguish0:196 [binder, in FreeSpec.Core.Interface]
Distinguish0:222 [binder, in FreeSpec.Core.Interface]
Distinguish0:250 [binder, in FreeSpec.Core.Interface]
Distinguish0:287 [binder, in FreeSpec.Core.Interface]
Distinguish10:206 [binder, in FreeSpec.Core.Interface]
Distinguish10:232 [binder, in FreeSpec.Core.Interface]
Distinguish10:260 [binder, in FreeSpec.Core.Interface]
Distinguish10:297 [binder, in FreeSpec.Core.Interface]
Distinguish11:207 [binder, in FreeSpec.Core.Interface]
Distinguish11:233 [binder, in FreeSpec.Core.Interface]
Distinguish11:261 [binder, in FreeSpec.Core.Interface]
Distinguish11:298 [binder, in FreeSpec.Core.Interface]
Distinguish12:262 [binder, in FreeSpec.Core.Interface]
Distinguish12:299 [binder, in FreeSpec.Core.Interface]
Distinguish13:263 [binder, in FreeSpec.Core.Interface]
Distinguish13:300 [binder, in FreeSpec.Core.Interface]
Distinguish14:264 [binder, in FreeSpec.Core.Interface]
Distinguish14:301 [binder, in FreeSpec.Core.Interface]
Distinguish15:265 [binder, in FreeSpec.Core.Interface]
Distinguish15:302 [binder, in FreeSpec.Core.Interface]
Distinguish16:266 [binder, in FreeSpec.Core.Interface]
Distinguish16:303 [binder, in FreeSpec.Core.Interface]
Distinguish17:267 [binder, in FreeSpec.Core.Interface]
Distinguish17:304 [binder, in FreeSpec.Core.Interface]
Distinguish18:268 [binder, in FreeSpec.Core.Interface]
Distinguish18:305 [binder, in FreeSpec.Core.Interface]
Distinguish19:269 [binder, in FreeSpec.Core.Interface]
Distinguish19:306 [binder, in FreeSpec.Core.Interface]
Distinguish1:139 [binder, in FreeSpec.Core.Interface]
Distinguish1:149 [binder, in FreeSpec.Core.Interface]
Distinguish1:161 [binder, in FreeSpec.Core.Interface]
Distinguish1:178 [binder, in FreeSpec.Core.Interface]
Distinguish1:197 [binder, in FreeSpec.Core.Interface]
Distinguish1:223 [binder, in FreeSpec.Core.Interface]
Distinguish1:251 [binder, in FreeSpec.Core.Interface]
Distinguish1:288 [binder, in FreeSpec.Core.Interface]
Distinguish2:162 [binder, in FreeSpec.Core.Interface]
Distinguish2:179 [binder, in FreeSpec.Core.Interface]
Distinguish2:198 [binder, in FreeSpec.Core.Interface]
Distinguish2:224 [binder, in FreeSpec.Core.Interface]
Distinguish2:252 [binder, in FreeSpec.Core.Interface]
Distinguish2:289 [binder, in FreeSpec.Core.Interface]
Distinguish3:163 [binder, in FreeSpec.Core.Interface]
Distinguish3:180 [binder, in FreeSpec.Core.Interface]
Distinguish3:199 [binder, in FreeSpec.Core.Interface]
Distinguish3:225 [binder, in FreeSpec.Core.Interface]
Distinguish3:253 [binder, in FreeSpec.Core.Interface]
Distinguish3:290 [binder, in FreeSpec.Core.Interface]
Distinguish4:164 [binder, in FreeSpec.Core.Interface]
Distinguish4:181 [binder, in FreeSpec.Core.Interface]
Distinguish4:200 [binder, in FreeSpec.Core.Interface]
Distinguish4:226 [binder, in FreeSpec.Core.Interface]
Distinguish4:254 [binder, in FreeSpec.Core.Interface]
Distinguish4:291 [binder, in FreeSpec.Core.Interface]
Distinguish5:165 [binder, in FreeSpec.Core.Interface]
Distinguish5:182 [binder, in FreeSpec.Core.Interface]
Distinguish5:201 [binder, in FreeSpec.Core.Interface]
Distinguish5:227 [binder, in FreeSpec.Core.Interface]
Distinguish5:255 [binder, in FreeSpec.Core.Interface]
Distinguish5:292 [binder, in FreeSpec.Core.Interface]
Distinguish6:202 [binder, in FreeSpec.Core.Interface]
Distinguish6:228 [binder, in FreeSpec.Core.Interface]
Distinguish6:256 [binder, in FreeSpec.Core.Interface]
Distinguish6:293 [binder, in FreeSpec.Core.Interface]
Distinguish7:203 [binder, in FreeSpec.Core.Interface]
Distinguish7:229 [binder, in FreeSpec.Core.Interface]
Distinguish7:257 [binder, in FreeSpec.Core.Interface]
Distinguish7:294 [binder, in FreeSpec.Core.Interface]
Distinguish8:204 [binder, in FreeSpec.Core.Interface]
Distinguish8:230 [binder, in FreeSpec.Core.Interface]
Distinguish8:258 [binder, in FreeSpec.Core.Interface]
Distinguish8:295 [binder, in FreeSpec.Core.Interface]
Distinguish9:205 [binder, in FreeSpec.Core.Interface]
Distinguish9:231 [binder, in FreeSpec.Core.Interface]
Distinguish9:259 [binder, in FreeSpec.Core.Interface]
Distinguish9:296 [binder, in FreeSpec.Core.Interface]
door [inductive, in FreeSpec.Example.airlock]
DOORS [inductive, in FreeSpec.Example.airlock]
doors_contract [definition, in FreeSpec.Example.airlock]
doors_o_callee_toggle [constructor, in FreeSpec.Example.airlock]
doors_o_callee_is_open [constructor, in FreeSpec.Example.airlock]
doors_o_callee [inductive, in FreeSpec.Example.airlock]
doors_o_caller [inductive, in FreeSpec.Example.airlock]
door_eq_dec [definition, in FreeSpec.Example.airlock]
do_no_use [definition, in FreeSpec.Core.Contract]
DRAM [inductive, in FreeSpec.Example.smram]
dram_specs [definition, in FreeSpec.Example.smram]
dram_o_callee [inductive, in FreeSpec.Example.smram]
dram_write_to [definition, in FreeSpec.Example.smram]
dram_read_from [definition, in FreeSpec.Example.smram]
d':4 [binder, in FreeSpec.Example.airlock]
d':99 [binder, in FreeSpec.Example.airlock]
d:10 [binder, in FreeSpec.Example.airlock]
d:14 [binder, in FreeSpec.Example.airlock]
d:18 [binder, in FreeSpec.Example.airlock]
d:23 [binder, in FreeSpec.Example.airlock]
d:27 [binder, in FreeSpec.Example.airlock]
d:3 [binder, in FreeSpec.Example.airlock]
d:34 [binder, in FreeSpec.Example.airlock]
d:35 [binder, in FreeSpec.Example.airlock]
d:45 [binder, in FreeSpec.Example.airlock]
d:47 [binder, in FreeSpec.Example.airlock]
d:50 [binder, in FreeSpec.Example.airlock]
d:52 [binder, in FreeSpec.Example.airlock]
d:62 [binder, in FreeSpec.Example.airlock]
d:64 [binder, in FreeSpec.Example.airlock]
d:70 [binder, in FreeSpec.Example.airlock]
d:74 [binder, in FreeSpec.Example.airlock]
d:81 [binder, in FreeSpec.Example.airlock]
d:86 [binder, in FreeSpec.Example.airlock]
d:92 [binder, in FreeSpec.Example.airlock]
d:97 [binder, in FreeSpec.Example.airlock]

E

equ:10 [binder, in FreeSpec.Core.ImpureFacts]
equ:73 [binder, in FreeSpec.Example.airlock]
equ:99 [binder, in FreeSpec.Core.Contract]
eval [definition, in FreeSpec.Exec.Eval]
Eval [constructor, in FreeSpec.Exec.Eval]
EVAL [inductive, in FreeSpec.Exec.Eval]
Eval [library]
eval_impure [definition, in FreeSpec.Core.Semantics]
eval_effect [definition, in FreeSpec.Core.Semantics]
eval_impure_Proper [instance, in FreeSpec.Core.SemanticsFacts]
eval_impure_bind_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
eval_impure_request_then_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
eval_semprod_in_right_eq [lemma, in FreeSpec.Core.SemanticsFacts]
eval_semprod_in_left_eq [lemma, in FreeSpec.Core.SemanticsFacts]
eval_effect_Proper [instance, in FreeSpec.Core.SemanticsFacts]
Exec [library]
exec_impure [definition, in FreeSpec.Core.Semantics]
exec_effect [definition, in FreeSpec.Core.Semantics]
exec_impure_Proper [instance, in FreeSpec.Core.SemanticsFacts]
exec_impure_bind_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
exec_impure_request_then_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
exec_semprod_in_right_eq [lemma, in FreeSpec.Core.SemanticsFacts]
exec_semprod_in_left_eq [lemma, in FreeSpec.Core.SemanticsFacts]
exec_effect_Proper [instance, in FreeSpec.Core.SemanticsFacts]
Extraction [library]
e:11 [binder, in FreeSpec.Core.SemanticsFacts]
e:11 [binder, in FreeSpec.Core.Interface]
e:114 [binder, in FreeSpec.Core.SemanticsFacts]
e:120 [binder, in FreeSpec.Core.SemanticsFacts]
e:126 [binder, in FreeSpec.Core.SemanticsFacts]
e:13 [binder, in FreeSpec.Core.Semantics]
e:14 [binder, in FreeSpec.Core.SemanticsFacts]
e:16 [binder, in FreeSpec.Core.Contract]
e:18 [binder, in FreeSpec.Core.Semantics]
e:18 [binder, in FreeSpec.Core.Interface]
e:21 [binder, in FreeSpec.Core.Interface]
e:22 [binder, in FreeSpec.Core.Contract]
e:22 [binder, in FreeSpec.Example.smram]
e:23 [binder, in FreeSpec.Core.Semantics]
e:25 [binder, in FreeSpec.Core.SemanticsFacts]
e:26 [binder, in FreeSpec.Core.ComponentFacts]
e:27 [binder, in FreeSpec.Core.Semantics]
e:29 [binder, in FreeSpec.Core.Contract]
e:31 [binder, in FreeSpec.Core.Semantics]
e:31 [binder, in FreeSpec.Core.HoareFacts]
e:312 [binder, in FreeSpec.Core.Interface]
e:313 [binder, in FreeSpec.Core.Interface]
e:315 [binder, in FreeSpec.Core.Interface]
e:318 [binder, in FreeSpec.Core.Interface]
e:323 [binder, in FreeSpec.Core.Interface]
e:33 [binder, in FreeSpec.Core.Interface]
e:331 [binder, in FreeSpec.Core.Interface]
e:336 [binder, in FreeSpec.Core.Interface]
e:343 [binder, in FreeSpec.Core.Interface]
e:35 [binder, in FreeSpec.Example.smram]
e:36 [binder, in FreeSpec.Core.SemanticsFacts]
e:37 [binder, in FreeSpec.Core.Semantics]
e:38 [binder, in FreeSpec.Core.Contract]
e:39 [binder, in FreeSpec.Core.ImpureFacts]
e:40 [binder, in FreeSpec.Core.Impure]
e:45 [binder, in FreeSpec.Core.Semantics]
e:46 [binder, in FreeSpec.Core.Hoare]
e:47 [binder, in FreeSpec.Core.Contract]
e:51 [binder, in FreeSpec.Core.SemanticsFacts]
e:54 [binder, in FreeSpec.Core.SemanticsFacts]
e:56 [binder, in FreeSpec.Core.Contract]
e:56 [binder, in FreeSpec.Example.airlock]
e:64 [binder, in FreeSpec.Core.Contract]
e:7 [binder, in FreeSpec.Core.ImpureFacts]
e:7 [binder, in FreeSpec.Core.Semantics]
e:7 [binder, in FreeSpec.Core.Instrument]
e:7 [binder, in FreeSpec.Core.Impure]
e:79 [binder, in FreeSpec.Core.Contract]
e:80 [binder, in FreeSpec.Core.SemanticsFacts]
e:83 [binder, in FreeSpec.Core.Contract]
e:86 [binder, in FreeSpec.Core.Contract]
e:86 [binder, in FreeSpec.Core.SemanticsFacts]
e:91 [binder, in FreeSpec.Core.Contract]
e:92 [binder, in FreeSpec.Core.SemanticsFacts]
e:98 [binder, in FreeSpec.Core.SemanticsFacts]

F

FFI [library]
finalizer:29 [binder, in FreeSpec.Core.Component]
forbid_specs [definition, in FreeSpec.Core.Contract]
FreeSpec_Inject [instance, in FreeSpec.FFI.FFI]
fst_Proper [instance, in FreeSpec.Core.SemanticsFacts]
function_eq_Equivalence [instance, in FreeSpec.Core.Init]
function_eq [definition, in FreeSpec.Core.Init]
f:10 [binder, in FreeSpec.Core.Init]
f:115 [binder, in FreeSpec.Core.SemanticsFacts]
f:121 [binder, in FreeSpec.Core.SemanticsFacts]
f:127 [binder, in FreeSpec.Core.SemanticsFacts]
f:13 [binder, in FreeSpec.Core.Impure]
f:133 [binder, in FreeSpec.Core.SemanticsFacts]
f:139 [binder, in FreeSpec.Core.SemanticsFacts]
f:145 [binder, in FreeSpec.Core.SemanticsFacts]
f:20 [binder, in FreeSpec.Core.Impure]
f:28 [binder, in FreeSpec.Core.Hoare]
f:32 [binder, in FreeSpec.Core.HoareFacts]
f:32 [binder, in FreeSpec.Core.Impure]
f:34 [binder, in FreeSpec.Core.ImpureFacts]
f:37 [binder, in FreeSpec.Core.Hoare]
f:41 [binder, in FreeSpec.Core.ImpureFacts]
f:47 [binder, in FreeSpec.Core.HoareFacts]
f:5 [binder, in FreeSpec.Core.Semantics]
f:61 [binder, in FreeSpec.Core.HoareFacts]
f:8 [binder, in FreeSpec.Core.ImpureFacts]
f:8 [binder, in FreeSpec.Core.Impure]

G

gen_callee_obligation [definition, in FreeSpec.Core.Contract]
gen_caller_obligation [definition, in FreeSpec.Core.Contract]
gen_witness_update [definition, in FreeSpec.Core.Contract]
Get [constructor, in FreeSpec.Core.Interface]
get_o_callee [constructor, in FreeSpec.Core.Contract]
g:11 [binder, in FreeSpec.Core.Init]
g:35 [binder, in FreeSpec.Core.ImpureFacts]
g:43 [binder, in FreeSpec.Core.ImpureFacts]
g:9 [binder, in FreeSpec.Core.ImpureFacts]

H

heap [library]
hf:35 [binder, in FreeSpec.Core.Hoare]
hoare [record, in FreeSpec.Core.Hoare]
Hoare [library]
HoareFacts [library]
hoare_Monad [instance, in FreeSpec.Core.Hoare]
hoare_Applicative [instance, in FreeSpec.Core.Hoare]
hoare_apply [definition, in FreeSpec.Core.Hoare]
hoare_Functor [instance, in FreeSpec.Core.Hoare]
hoare_map [definition, in FreeSpec.Core.Hoare]
hoare_bind [definition, in FreeSpec.Core.Hoare]
hoare_pure [definition, in FreeSpec.Core.Hoare]
hoare_Equivalence [instance, in FreeSpec.Core.HoareFacts]
hoare_eq [inductive, in FreeSpec.Core.HoareFacts]
hpost:110 [binder, in FreeSpec.Example.airlock]
hpre:109 [binder, in FreeSpec.Example.airlock]
hpre:34 [binder, in FreeSpec.Core.HoareFacts]
Hp:45 [binder, in FreeSpec.Core.HoareFacts]
Hp:65 [binder, in FreeSpec.Core.HoareFacts]
H0:102 [binder, in FreeSpec.Example.airlock]
H0:105 [binder, in FreeSpec.Core.Interface]
H0:118 [binder, in FreeSpec.Core.Interface]
H0:13 [binder, in FreeSpec.Example.airlock]
H0:135 [binder, in FreeSpec.Core.Interface]
H0:144 [binder, in FreeSpec.Core.Interface]
H0:155 [binder, in FreeSpec.Core.Interface]
H0:17 [binder, in FreeSpec.Example.airlock]
H0:170 [binder, in FreeSpec.Core.Interface]
H0:189 [binder, in FreeSpec.Core.Interface]
H0:212 [binder, in FreeSpec.Core.Interface]
H0:22 [binder, in FreeSpec.Example.airlock]
H0:241 [binder, in FreeSpec.Core.Interface]
H0:25 [binder, in FreeSpec.Example.smram]
H0:278 [binder, in FreeSpec.Core.Interface]
H0:29 [binder, in FreeSpec.Example.smram]
H0:29 [binder, in FreeSpec.Core.Interface]
H0:3 [binder, in FreeSpec.Example.heap]
H0:30 [binder, in FreeSpec.Example.airlock]
H0:329 [binder, in FreeSpec.Core.Interface]
H0:33 [binder, in FreeSpec.Example.airlock]
H0:342 [binder, in FreeSpec.Core.Interface]
H0:38 [binder, in FreeSpec.Example.smram]
H0:38 [binder, in FreeSpec.Core.Impure]
H0:39 [binder, in FreeSpec.Example.airlock]
H0:39 [binder, in FreeSpec.Core.Interface]
H0:42 [binder, in FreeSpec.Example.smram]
H0:45 [binder, in FreeSpec.Core.Impure]
H0:46 [binder, in FreeSpec.Core.Interface]
H0:55 [binder, in FreeSpec.Core.Interface]
H0:64 [binder, in FreeSpec.Core.Interface]
H0:69 [binder, in FreeSpec.Core.Contract]
H0:7 [binder, in FreeSpec.Exec.Eval]
H0:71 [binder, in FreeSpec.Core.HoareFacts]
H0:77 [binder, in FreeSpec.Core.Interface]
H0:79 [binder, in FreeSpec.Example.airlock]
H0:8 [binder, in FreeSpec.Example.heap]
H0:84 [binder, in FreeSpec.Example.airlock]
H0:88 [binder, in FreeSpec.Core.Interface]
H0:9 [binder, in FreeSpec.Example.airlock]
H0:90 [binder, in FreeSpec.Example.airlock]
h1:3 [binder, in FreeSpec.Core.HoareFacts]
H1:30 [binder, in FreeSpec.Core.Interface]
H2:107 [binder, in FreeSpec.Core.Interface]
H2:121 [binder, in FreeSpec.Core.Interface]
H2:137 [binder, in FreeSpec.Core.Interface]
H2:147 [binder, in FreeSpec.Core.Interface]
H2:157 [binder, in FreeSpec.Core.Interface]
H2:173 [binder, in FreeSpec.Core.Interface]
H2:191 [binder, in FreeSpec.Core.Interface]
H2:215 [binder, in FreeSpec.Core.Interface]
H2:243 [binder, in FreeSpec.Core.Interface]
H2:280 [binder, in FreeSpec.Core.Interface]
h2:4 [binder, in FreeSpec.Core.HoareFacts]
H2:41 [binder, in FreeSpec.Example.airlock]
H2:41 [binder, in FreeSpec.Core.Interface]
H2:49 [binder, in FreeSpec.Core.Interface]
H2:57 [binder, in FreeSpec.Core.Interface]
H2:67 [binder, in FreeSpec.Core.Interface]
H2:72 [binder, in FreeSpec.Core.Contract]
H2:74 [binder, in FreeSpec.Core.HoareFacts]
H2:79 [binder, in FreeSpec.Core.Interface]
H2:91 [binder, in FreeSpec.Core.Interface]
H3:118 [binder, in FreeSpec.Example.airlock]
H4:109 [binder, in FreeSpec.Core.Interface]
H4:124 [binder, in FreeSpec.Core.Interface]
H4:159 [binder, in FreeSpec.Core.Interface]
H4:176 [binder, in FreeSpec.Core.Interface]
H4:193 [binder, in FreeSpec.Core.Interface]
H4:218 [binder, in FreeSpec.Core.Interface]
H4:245 [binder, in FreeSpec.Core.Interface]
H4:282 [binder, in FreeSpec.Core.Interface]
H4:59 [binder, in FreeSpec.Core.Interface]
H4:70 [binder, in FreeSpec.Core.Interface]
H4:81 [binder, in FreeSpec.Core.Interface]
H4:94 [binder, in FreeSpec.Core.Interface]
H5:134 [binder, in FreeSpec.Example.smram]
H5:151 [binder, in FreeSpec.Example.smram]
H5:65 [binder, in FreeSpec.Example.smram]
H5:77 [binder, in FreeSpec.Example.smram]
H6:111 [binder, in FreeSpec.Core.Interface]
H6:127 [binder, in FreeSpec.Core.Interface]
H6:195 [binder, in FreeSpec.Core.Interface]
H6:221 [binder, in FreeSpec.Core.Interface]
H6:247 [binder, in FreeSpec.Core.Interface]
H6:284 [binder, in FreeSpec.Core.Interface]
H6:83 [binder, in FreeSpec.Core.Interface]
H6:97 [binder, in FreeSpec.Core.Interface]
H8:113 [binder, in FreeSpec.Core.Interface]
H8:130 [binder, in FreeSpec.Core.Interface]
H8:249 [binder, in FreeSpec.Core.Interface]
H8:286 [binder, in FreeSpec.Core.Interface]
H:103 [binder, in FreeSpec.Core.SemanticsFacts]
H:12 [binder, in FreeSpec.Core.Instrument]
H:12 [binder, in FreeSpec.Core.InstrumentFacts]
H:14 [binder, in FreeSpec.Core.ComponentFacts]
h:15 [binder, in FreeSpec.Core.Hoare]
H:15 [binder, in FreeSpec.Core.Init]
H:15 [binder, in FreeSpec.Core.Interface]
H:2 [binder, in FreeSpec.Core.Init]
H:2 [binder, in FreeSpec.Example.heap]
H:20 [binder, in FreeSpec.Core.SemanticsFacts]
H:21 [binder, in FreeSpec.Core.InstrumentFacts]
H:23 [binder, in FreeSpec.FFI.Refs]
H:27 [binder, in FreeSpec.Core.HoareFacts]
H:27 [binder, in FreeSpec.FFI.Refs]
h:29 [binder, in FreeSpec.Core.Hoare]
H:3 [binder, in FreeSpec.Core.Instrument]
H:3 [binder, in FreeSpec.Core.SemanticsFacts]
H:3 [binder, in FreeSpec.Core.InstrumentFacts]
H:31 [binder, in FreeSpec.Core.SemanticsFacts]
H:31 [binder, in FreeSpec.FFI.Refs]
H:31 [binder, in FreeSpec.Core.InstrumentFacts]
H:322 [binder, in FreeSpec.Core.Interface]
H:33 [binder, in FreeSpec.Core.ComponentFacts]
H:335 [binder, in FreeSpec.Core.Interface]
h:36 [binder, in FreeSpec.Core.Hoare]
H:36 [binder, in FreeSpec.FFI.Refs]
H:379 [binder, in FreeSpec.Core.Interface]
H:387 [binder, in FreeSpec.Core.Interface]
H:39 [binder, in FreeSpec.Core.HoareFacts]
H:4 [binder, in FreeSpec.FFI.FFI]
H:42 [binder, in FreeSpec.Core.Hoare]
H:42 [binder, in FreeSpec.Core.Contract]
H:42 [binder, in FreeSpec.Core.SemanticsFacts]
H:48 [binder, in FreeSpec.Core.Impure]
H:51 [binder, in FreeSpec.Core.Contract]
H:53 [binder, in FreeSpec.Core.Hoare]
H:55 [binder, in FreeSpec.Core.HoareFacts]
H:59 [binder, in FreeSpec.Core.Contract]
H:66 [binder, in FreeSpec.Example.airlock]

I

iempty [inductive, in FreeSpec.Core.Interface]
iempty_semantics [definition, in FreeSpec.Core.Semantics]
impure [inductive, in FreeSpec.Core.Impure]
Impure [library]
ImpureFacts [library]
impure_bind_assoc [lemma, in FreeSpec.Core.ImpureFacts]
impure_bind_local [lemma, in FreeSpec.Core.ImpureFacts]
impure_apply_Proper [instance, in FreeSpec.Core.ImpureFacts]
impure_map_Proper [instance, in FreeSpec.Core.ImpureFacts]
impure_bind_Proper [instance, in FreeSpec.Core.ImpureFacts]
impure_Equivalence [instance, in FreeSpec.Core.ImpureFacts]
impure_eq [inductive, in FreeSpec.Core.ImpureFacts]
impure_lift [definition, in FreeSpec.Core.Impure]
impure_Monad [instance, in FreeSpec.Core.Impure]
impure_Applicative [instance, in FreeSpec.Core.Impure]
impure_apply [definition, in FreeSpec.Core.Impure]
impure_pure [definition, in FreeSpec.Core.Impure]
impure_Functor [instance, in FreeSpec.Core.Impure]
impure_map [definition, in FreeSpec.Core.Impure]
impure_bind [definition, in FreeSpec.Core.Impure]
Init [library]
initializer:27 [binder, in FreeSpec.Core.Component]
init:10 [binder, in FreeSpec.Core.Semantics]
init:24 [binder, in FreeSpec.Core.ComponentFacts]
inj_assign [definition, in FreeSpec.FFI.Refs]
inj_deref [definition, in FreeSpec.FFI.Refs]
inj_make_ref [definition, in FreeSpec.FFI.Refs]
inj_p [projection, in FreeSpec.Core.Interface]
instrument [abbreviation, in FreeSpec.Core.Instrument]
Instrument [library]
InstrumentFacts [library]
instrument_to_state [definition, in FreeSpec.Core.Instrument]
instrument_preserves_compliance [lemma, in FreeSpec.Core.InstrumentFacts]
instrument_satisfies_hoare [lemma, in FreeSpec.Core.InstrumentFacts]
instrument_to_state_exec_morphism [lemma, in FreeSpec.Core.InstrumentFacts]
instrument_to_state_eval_morphism [lemma, in FreeSpec.Core.InstrumentFacts]
instr:19 [binder, in FreeSpec.Core.Instrument]
interface [definition, in FreeSpec.Core.Interface]
Interface [library]
interface_to_hoare [definition, in FreeSpec.Core.Hoare]
interface_to_state [definition, in FreeSpec.Core.Semantics]
interface_to_instrument [definition, in FreeSpec.Core.Instrument]
interp [abbreviation, in FreeSpec.Core.Semantics]
inv:44 [binder, in FreeSpec.Core.ComponentFacts]
in_smram_morphism [axiom, in FreeSpec.Example.smram]
in_smram [axiom, in FreeSpec.Example.smram]
in_right [constructor, in FreeSpec.Core.Interface]
in_left [constructor, in FreeSpec.Core.Interface]
io_assign [axiom, in FreeSpec.FFI.Refs]
io_deref [axiom, in FreeSpec.FFI.Refs]
io_make_ref [axiom, in FreeSpec.FFI.Refs]
iplus [inductive, in FreeSpec.Core.Interface]
iplus_right_distinguish_right_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_left_distinguish_left_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_right_may_left_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_left_may_right_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_right_default_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_left_default_Distinguish [instance, in FreeSpec.Core.Interface]
iplus_right_Provide [instance, in FreeSpec.Core.Interface]
iplus_right_MayProvide [instance, in FreeSpec.Core.Interface]
iplus_left_Provide [instance, in FreeSpec.Core.Interface]
iplus_left_MayProvide [instance, in FreeSpec.Core.Interface]
IsOpen [constructor, in FreeSpec.Example.airlock]
is_open [definition, in FreeSpec.Example.airlock]
ix:1 [binder, in FreeSpec.FFI.FFI]
ix:1 [binder, in FreeSpec.Core.Instrument]
ix:1 [binder, in FreeSpec.Core.SemanticsFacts]
ix:1 [binder, in FreeSpec.Core.InstrumentFacts]
ix:10 [binder, in FreeSpec.Core.Instrument]
ix:10 [binder, in FreeSpec.Core.InstrumentFacts]
ix:100 [binder, in FreeSpec.Example.airlock]
ix:101 [binder, in FreeSpec.Core.SemanticsFacts]
ix:11 [binder, in FreeSpec.Example.airlock]
ix:111 [binder, in FreeSpec.Example.airlock]
ix:115 [binder, in FreeSpec.Core.Interface]
ix:121 [binder, in FreeSpec.Example.smram]
ix:13 [binder, in FreeSpec.Core.Interface]
ix:131 [binder, in FreeSpec.Core.Interface]
ix:138 [binder, in FreeSpec.Example.smram]
ix:141 [binder, in FreeSpec.Core.Interface]
ix:15 [binder, in FreeSpec.Example.airlock]
ix:15 [binder, in FreeSpec.Core.Component]
ix:150 [binder, in FreeSpec.Core.Interface]
ix:167 [binder, in FreeSpec.Core.Interface]
ix:18 [binder, in FreeSpec.Core.SemanticsFacts]
ix:183 [binder, in FreeSpec.Core.Interface]
ix:19 [binder, in FreeSpec.Core.InstrumentFacts]
ix:20 [binder, in FreeSpec.Example.airlock]
ix:209 [binder, in FreeSpec.Core.Interface]
ix:23 [binder, in FreeSpec.Example.smram]
ix:234 [binder, in FreeSpec.Core.Interface]
ix:24 [binder, in FreeSpec.Core.Component]
ix:25 [binder, in FreeSpec.Core.HoareFacts]
ix:25 [binder, in FreeSpec.Core.Interface]
ix:27 [binder, in FreeSpec.Example.smram]
ix:271 [binder, in FreeSpec.Core.Interface]
ix:28 [binder, in FreeSpec.Example.airlock]
ix:29 [binder, in FreeSpec.Core.SemanticsFacts]
ix:29 [binder, in FreeSpec.Core.InstrumentFacts]
ix:31 [binder, in FreeSpec.Example.airlock]
ix:319 [binder, in FreeSpec.Core.Interface]
ix:325 [binder, in FreeSpec.Core.Interface]
ix:346 [binder, in FreeSpec.Core.Interface]
ix:35 [binder, in FreeSpec.Core.Impure]
ix:35 [binder, in FreeSpec.Core.Interface]
ix:352 [binder, in FreeSpec.Core.Interface]
ix:358 [binder, in FreeSpec.Core.Interface]
ix:36 [binder, in FreeSpec.Example.smram]
ix:365 [binder, in FreeSpec.Core.Interface]
ix:37 [binder, in FreeSpec.Core.HoareFacts]
ix:37 [binder, in FreeSpec.Example.airlock]
ix:372 [binder, in FreeSpec.Core.Interface]
ix:380 [binder, in FreeSpec.Core.Interface]
ix:40 [binder, in FreeSpec.Core.Hoare]
ix:40 [binder, in FreeSpec.Core.Contract]
ix:40 [binder, in FreeSpec.Example.smram]
ix:40 [binder, in FreeSpec.Core.SemanticsFacts]
ix:43 [binder, in FreeSpec.Core.Impure]
ix:43 [binder, in FreeSpec.Core.Interface]
ix:49 [binder, in FreeSpec.Core.Contract]
ix:5 [binder, in FreeSpec.Exec.Eval]
ix:50 [binder, in FreeSpec.Core.Interface]
ix:51 [binder, in FreeSpec.Core.Hoare]
ix:53 [binder, in FreeSpec.Core.HoareFacts]
ix:57 [binder, in FreeSpec.Core.Contract]
ix:58 [binder, in FreeSpec.Example.smram]
ix:6 [binder, in FreeSpec.Example.heap]
ix:60 [binder, in FreeSpec.Core.Semantics]
ix:61 [binder, in FreeSpec.Core.Interface]
ix:66 [binder, in FreeSpec.Core.Contract]
ix:68 [binder, in FreeSpec.Core.HoareFacts]
ix:7 [binder, in FreeSpec.Example.airlock]
ix:7 [binder, in FreeSpec.Core.Interface]
ix:70 [binder, in FreeSpec.Core.Semantics]
ix:70 [binder, in FreeSpec.Example.smram]
ix:71 [binder, in FreeSpec.Core.Interface]
ix:77 [binder, in FreeSpec.Example.airlock]
ix:82 [binder, in FreeSpec.Example.airlock]
ix:85 [binder, in FreeSpec.Core.Interface]
ix:88 [binder, in FreeSpec.Example.airlock]
ix:98 [binder, in FreeSpec.Core.Interface]
i1:116 [binder, in FreeSpec.Core.Interface]
i1:132 [binder, in FreeSpec.Core.Interface]
i1:142 [binder, in FreeSpec.Core.Interface]
i1:151 [binder, in FreeSpec.Core.Interface]
i1:168 [binder, in FreeSpec.Core.Interface]
i1:184 [binder, in FreeSpec.Core.Interface]
i1:210 [binder, in FreeSpec.Core.Interface]
i1:235 [binder, in FreeSpec.Core.Interface]
i1:272 [binder, in FreeSpec.Core.Interface]
i1:36 [binder, in FreeSpec.Core.Interface]
i1:44 [binder, in FreeSpec.Core.Interface]
i1:51 [binder, in FreeSpec.Core.Interface]
i1:62 [binder, in FreeSpec.Core.Interface]
i1:72 [binder, in FreeSpec.Core.Interface]
i1:86 [binder, in FreeSpec.Core.Interface]
i1:99 [binder, in FreeSpec.Core.Interface]
i2:100 [binder, in FreeSpec.Core.Interface]
i2:119 [binder, in FreeSpec.Core.Interface]
i2:133 [binder, in FreeSpec.Core.Interface]
i2:145 [binder, in FreeSpec.Core.Interface]
i2:152 [binder, in FreeSpec.Core.Interface]
i2:171 [binder, in FreeSpec.Core.Interface]
i2:185 [binder, in FreeSpec.Core.Interface]
i2:213 [binder, in FreeSpec.Core.Interface]
i2:236 [binder, in FreeSpec.Core.Interface]
i2:273 [binder, in FreeSpec.Core.Interface]
i2:37 [binder, in FreeSpec.Core.Interface]
i2:47 [binder, in FreeSpec.Core.Interface]
i2:52 [binder, in FreeSpec.Core.Interface]
i2:65 [binder, in FreeSpec.Core.Interface]
i2:73 [binder, in FreeSpec.Core.Interface]
i2:89 [binder, in FreeSpec.Core.Interface]
i3:101 [binder, in FreeSpec.Core.Interface]
i3:122 [binder, in FreeSpec.Core.Interface]
i3:153 [binder, in FreeSpec.Core.Interface]
i3:174 [binder, in FreeSpec.Core.Interface]
i3:186 [binder, in FreeSpec.Core.Interface]
i3:216 [binder, in FreeSpec.Core.Interface]
i3:237 [binder, in FreeSpec.Core.Interface]
i3:274 [binder, in FreeSpec.Core.Interface]
i3:53 [binder, in FreeSpec.Core.Interface]
i3:68 [binder, in FreeSpec.Core.Interface]
i3:74 [binder, in FreeSpec.Core.Interface]
i3:92 [binder, in FreeSpec.Core.Interface]
i4:102 [binder, in FreeSpec.Core.Interface]
i4:125 [binder, in FreeSpec.Core.Interface]
i4:187 [binder, in FreeSpec.Core.Interface]
i4:219 [binder, in FreeSpec.Core.Interface]
i4:238 [binder, in FreeSpec.Core.Interface]
i4:275 [binder, in FreeSpec.Core.Interface]
i4:75 [binder, in FreeSpec.Core.Interface]
i4:95 [binder, in FreeSpec.Core.Interface]
i5:103 [binder, in FreeSpec.Core.Interface]
i5:128 [binder, in FreeSpec.Core.Interface]
i5:239 [binder, in FreeSpec.Core.Interface]
i5:276 [binder, in FreeSpec.Core.Interface]
i:1 [binder, in FreeSpec.Core.ComponentFacts]
i:1 [binder, in FreeSpec.Core.Contract]
i:1 [binder, in FreeSpec.Core.ImpureFacts]
i:1 [binder, in FreeSpec.Core.Semantics]
i:1 [binder, in FreeSpec.Core.Component]
i:1 [binder, in FreeSpec.Core.Impure]
i:102 [binder, in FreeSpec.Core.SemanticsFacts]
i:106 [binder, in FreeSpec.Core.SemanticsFacts]
i:11 [binder, in FreeSpec.Core.Instrument]
i:11 [binder, in FreeSpec.Core.InstrumentFacts]
i:110 [binder, in FreeSpec.Core.SemanticsFacts]
i:116 [binder, in FreeSpec.Core.SemanticsFacts]
i:122 [binder, in FreeSpec.Core.SemanticsFacts]
i:128 [binder, in FreeSpec.Core.SemanticsFacts]
i:13 [binder, in FreeSpec.Core.Contract]
i:13 [binder, in FreeSpec.Core.Component]
i:134 [binder, in FreeSpec.Core.SemanticsFacts]
i:14 [binder, in FreeSpec.Core.Interface]
i:140 [binder, in FreeSpec.Core.SemanticsFacts]
i:146 [binder, in FreeSpec.Core.SemanticsFacts]
i:148 [binder, in FreeSpec.Core.SemanticsFacts]
i:15 [binder, in FreeSpec.Core.ComponentFacts]
i:15 [binder, in FreeSpec.Core.Semantics]
i:15 [binder, in FreeSpec.Core.Instrument]
i:150 [binder, in FreeSpec.Core.SemanticsFacts]
i:152 [binder, in FreeSpec.Core.SemanticsFacts]
i:17 [binder, in FreeSpec.Core.Impure]
i:18 [binder, in FreeSpec.Core.Contract]
i:19 [binder, in FreeSpec.Core.SemanticsFacts]
i:2 [binder, in FreeSpec.FFI.FFI]
i:2 [binder, in FreeSpec.Core.Instrument]
i:2 [binder, in FreeSpec.Core.SemanticsFacts]
i:2 [binder, in FreeSpec.Core.InstrumentFacts]
i:20 [binder, in FreeSpec.Core.Semantics]
i:20 [binder, in FreeSpec.Core.InstrumentFacts]
i:23 [binder, in FreeSpec.Core.Interface]
i:24 [binder, in FreeSpec.Core.Semantics]
i:24 [binder, in FreeSpec.Core.Impure]
i:25 [binder, in FreeSpec.Core.Contract]
i:25 [binder, in FreeSpec.Core.ImpureFacts]
i:26 [binder, in FreeSpec.Core.HoareFacts]
i:26 [binder, in FreeSpec.Core.Interface]
i:27 [binder, in FreeSpec.Core.Impure]
i:28 [binder, in FreeSpec.Core.Semantics]
i:29 [binder, in FreeSpec.Core.ImpureFacts]
i:30 [binder, in FreeSpec.Core.SemanticsFacts]
i:30 [binder, in FreeSpec.Core.InstrumentFacts]
i:307 [binder, in FreeSpec.Core.Interface]
i:314 [binder, in FreeSpec.Core.Interface]
i:316 [binder, in FreeSpec.Core.Interface]
i:32 [binder, in FreeSpec.Core.Semantics]
i:320 [binder, in FreeSpec.Core.Interface]
i:326 [binder, in FreeSpec.Core.Interface]
i:33 [binder, in FreeSpec.Core.Contract]
i:332 [binder, in FreeSpec.Core.Interface]
i:338 [binder, in FreeSpec.Core.Interface]
i:34 [binder, in FreeSpec.Core.ComponentFacts]
i:34 [binder, in FreeSpec.Core.Contract]
i:34 [binder, in FreeSpec.Core.Impure]
i:344 [binder, in FreeSpec.Core.Interface]
i:348 [binder, in FreeSpec.Core.Interface]
i:354 [binder, in FreeSpec.Core.Interface]
i:36 [binder, in FreeSpec.Core.Impure]
i:360 [binder, in FreeSpec.Core.Interface]
i:367 [binder, in FreeSpec.Core.Interface]
i:37 [binder, in FreeSpec.Core.ImpureFacts]
i:374 [binder, in FreeSpec.Core.Interface]
i:38 [binder, in FreeSpec.Core.HoareFacts]
i:382 [binder, in FreeSpec.Core.Interface]
i:39 [binder, in FreeSpec.Core.Contract]
i:4 [binder, in FreeSpec.Core.Component]
i:41 [binder, in FreeSpec.Core.Hoare]
i:41 [binder, in FreeSpec.Core.Contract]
i:41 [binder, in FreeSpec.Core.SemanticsFacts]
i:43 [binder, in FreeSpec.Core.Semantics]
i:45 [binder, in FreeSpec.Core.SemanticsFacts]
i:47 [binder, in FreeSpec.Core.Semantics]
i:48 [binder, in FreeSpec.Core.Semantics]
i:49 [binder, in FreeSpec.Core.Impure]
i:50 [binder, in FreeSpec.Core.Contract]
i:52 [binder, in FreeSpec.Core.Hoare]
i:52 [binder, in FreeSpec.Core.Semantics]
i:54 [binder, in FreeSpec.Core.HoareFacts]
i:56 [binder, in FreeSpec.Core.Semantics]
i:56 [binder, in FreeSpec.Core.SemanticsFacts]
i:58 [binder, in FreeSpec.Core.Contract]
i:58 [binder, in FreeSpec.Core.SemanticsFacts]
i:67 [binder, in FreeSpec.Core.Contract]
i:69 [binder, in FreeSpec.Core.HoareFacts]
i:75 [binder, in FreeSpec.Core.SemanticsFacts]
i:8 [binder, in FreeSpec.Core.ComponentFacts]
i:8 [binder, in FreeSpec.Core.Interface]
i:81 [binder, in FreeSpec.Core.SemanticsFacts]
i:87 [binder, in FreeSpec.Core.SemanticsFacts]
i:9 [binder, in FreeSpec.Core.Impure]
i:93 [binder, in FreeSpec.Core.SemanticsFacts]
i:99 [binder, in FreeSpec.Core.SemanticsFacts]

J

jx:12 [binder, in FreeSpec.Core.ComponentFacts]
jx:31 [binder, in FreeSpec.Core.ComponentFacts]
jx:333 [binder, in FreeSpec.Core.Interface]
jx:339 [binder, in FreeSpec.Core.Interface]
jx:347 [binder, in FreeSpec.Core.Interface]
jx:353 [binder, in FreeSpec.Core.Interface]
jx:359 [binder, in FreeSpec.Core.Interface]
jx:366 [binder, in FreeSpec.Core.Interface]
jx:373 [binder, in FreeSpec.Core.Interface]
jx:381 [binder, in FreeSpec.Core.Interface]
j:100 [binder, in FreeSpec.Core.SemanticsFacts]
j:13 [binder, in FreeSpec.Core.ComponentFacts]
j:16 [binder, in FreeSpec.Core.Component]
j:2 [binder, in FreeSpec.Core.ComponentFacts]
j:2 [binder, in FreeSpec.Core.Component]
j:24 [binder, in FreeSpec.Core.Interface]
j:25 [binder, in FreeSpec.Core.Component]
j:27 [binder, in FreeSpec.Core.Interface]
j:308 [binder, in FreeSpec.Core.Interface]
j:32 [binder, in FreeSpec.Core.ComponentFacts]
j:321 [binder, in FreeSpec.Core.Interface]
j:327 [binder, in FreeSpec.Core.Interface]
j:33 [binder, in FreeSpec.Core.Semantics]
j:334 [binder, in FreeSpec.Core.Interface]
j:340 [binder, in FreeSpec.Core.Interface]
j:345 [binder, in FreeSpec.Core.Interface]
j:349 [binder, in FreeSpec.Core.Interface]
j:355 [binder, in FreeSpec.Core.Interface]
j:361 [binder, in FreeSpec.Core.Interface]
j:368 [binder, in FreeSpec.Core.Interface]
j:375 [binder, in FreeSpec.Core.Interface]
j:383 [binder, in FreeSpec.Core.Interface]
j:5 [binder, in FreeSpec.Core.Component]
j:61 [binder, in FreeSpec.Core.Semantics]
j:70 [binder, in FreeSpec.Core.Contract]
j:72 [binder, in FreeSpec.Core.HoareFacts]
j:77 [binder, in FreeSpec.Core.SemanticsFacts]
j:83 [binder, in FreeSpec.Core.SemanticsFacts]
j:89 [binder, in FreeSpec.Core.SemanticsFacts]
j:9 [binder, in FreeSpec.Core.ComponentFacts]
j:95 [binder, in FreeSpec.Core.SemanticsFacts]

K

k:16 [binder, in FreeSpec.Core.Hoare]

L

left [constructor, in FreeSpec.Example.airlock]
local [constructor, in FreeSpec.Core.Impure]
local_eq [constructor, in FreeSpec.Core.ImpureFacts]
l:50 [binder, in FreeSpec.Core.Impure]

M

MakeDRAM [constructor, in FreeSpec.Example.smram]
MakeVGA [constructor, in FreeSpec.Example.smram]
make_contract [constructor, in FreeSpec.Core.Contract]
Make_ref [constructor, in FreeSpec.FFI.Refs]
make_ref [projection, in FreeSpec.FFI.Refs]
Make_StrictProvide5 [instance, in FreeSpec.Core.Interface]
Make_StrictProvide4 [instance, in FreeSpec.Core.Interface]
Make_StrictProvide3 [instance, in FreeSpec.Core.Interface]
Make_StrictProvide2 [instance, in FreeSpec.Core.Interface]
Make_Provide5 [instance, in FreeSpec.Core.Interface]
Make_Provide4 [instance, in FreeSpec.Core.Interface]
Make_Provide3 [instance, in FreeSpec.Core.Interface]
Make_Provide2 [instance, in FreeSpec.Core.Interface]
MayProvide [record, in FreeSpec.Core.Interface]
mc_specs [definition, in FreeSpec.Example.smram]
MEMORY [inductive, in FreeSpec.Example.smram]
memory_controller_correct [lemma, in FreeSpec.Example.smram]
memory_controller_respectful [lemma, in FreeSpec.Example.smram]
memory_controller_write_o_callee [constructor, in FreeSpec.Example.smram]
memory_controller_read_o_callee [constructor, in FreeSpec.Example.smram]
memory_controller_o_callee [inductive, in FreeSpec.Example.smram]
memory_view [definition, in FreeSpec.Example.smram]
memory_controller [definition, in FreeSpec.Example.smram]
MEMORY_CONTROLLER [inductive, in FreeSpec.Example.smram]
mk_hoare [constructor, in FreeSpec.Core.Hoare]
mk_no_callee_obligation [constructor, in FreeSpec.Core.Contract]
mk_no_caller_obligation [constructor, in FreeSpec.Core.Contract]
mk_semantics [constructor, in FreeSpec.Core.Semantics]
mk_hoare_eq [constructor, in FreeSpec.Core.HoareFacts]
ML [library]
MonadRefs [record, in FreeSpec.FFI.Refs]
MonadRefs_Inject [instance, in FreeSpec.FFI.Refs]
MonadRefs_IO [instance, in FreeSpec.FFI.Refs]
M1:350 [binder, in FreeSpec.Core.Interface]
M1:356 [binder, in FreeSpec.Core.Interface]
M1:362 [binder, in FreeSpec.Core.Interface]
M1:369 [binder, in FreeSpec.Core.Interface]
M1:376 [binder, in FreeSpec.Core.Interface]
M1:384 [binder, in FreeSpec.Core.Interface]
M2:364 [binder, in FreeSpec.Core.Interface]
M2:371 [binder, in FreeSpec.Core.Interface]
M2:378 [binder, in FreeSpec.Core.Interface]
M2:386 [binder, in FreeSpec.Core.Interface]
m:1 [binder, in FreeSpec.Core.Init]
m:1 [binder, in FreeSpec.Example.heap]
m:22 [binder, in FreeSpec.FFI.Refs]
m:26 [binder, in FreeSpec.FFI.Refs]
m:3 [binder, in FreeSpec.FFI.Refs]
m:30 [binder, in FreeSpec.FFI.Refs]
m:35 [binder, in FreeSpec.FFI.Refs]
m:47 [binder, in FreeSpec.Core.Impure]

N

next_eq:55 [binder, in FreeSpec.Core.SemanticsFacts]
next:12 [binder, in FreeSpec.Core.Component]
next:15 [binder, in FreeSpec.Core.SemanticsFacts]
next:68 [binder, in FreeSpec.Core.Semantics]
no_contract [definition, in FreeSpec.Core.Contract]
no_callee_obligation [inductive, in FreeSpec.Core.Contract]
no_caller_obligation [inductive, in FreeSpec.Core.Contract]
no_contract_compliant_semantics [lemma, in FreeSpec.Core.SemanticsFacts]

O

one_door_safe_all_doors_safe [lemma, in FreeSpec.Example.airlock]
open_door_respectful [lemma, in FreeSpec.Example.airlock]
open_door [definition, in FreeSpec.Example.airlock]
open:19 [binder, in FreeSpec.Example.airlock]
open:24 [binder, in FreeSpec.Example.airlock]
op:136 [binder, in FreeSpec.Example.smram]
op:42 [binder, in FreeSpec.Example.airlock]
op:78 [binder, in FreeSpec.Example.smram]
out:40 [binder, in FreeSpec.Core.Semantics]
out:42 [binder, in FreeSpec.Core.Semantics]
o_caller:27 [binder, in FreeSpec.Core.ComponentFacts]
o_callee_store [inductive, in FreeSpec.Core.Contract]
o_caller:37 [binder, in FreeSpec.Core.SemanticsFacts]
o_caller:26 [binder, in FreeSpec.Core.SemanticsFacts]
o_callee:12 [binder, in FreeSpec.Core.SemanticsFacts]

P

pin:110 [binder, in FreeSpec.Example.smram]
pin:114 [binder, in FreeSpec.Example.smram]
pin:49 [binder, in FreeSpec.Example.smram]
pin:51 [binder, in FreeSpec.Example.smram]
post [projection, in FreeSpec.Core.Hoare]
post_Proper [instance, in FreeSpec.Core.HoareFacts]
post_eq:12 [binder, in FreeSpec.Core.HoareFacts]
pre [projection, in FreeSpec.Core.Hoare]
pred:21 [binder, in FreeSpec.Core.ComponentFacts]
pred:40 [binder, in FreeSpec.Core.ComponentFacts]
prei:82 [binder, in FreeSpec.Core.HoareFacts]
prej:84 [binder, in FreeSpec.Core.HoareFacts]
pre_Proper [instance, in FreeSpec.Core.HoareFacts]
pre_eq:8 [binder, in FreeSpec.Core.HoareFacts]
priv:68 [binder, in FreeSpec.Example.smram]
prod_Proper [instance, in FreeSpec.Core.SemanticsFacts]
proj_inj_p_equ [projection, in FreeSpec.Core.Interface]
proj_p [projection, in FreeSpec.Core.Interface]
prom:113 [binder, in FreeSpec.Example.smram]
prom:96 [binder, in FreeSpec.Example.smram]
Provide [record, in FreeSpec.Core.Interface]
Provide2 [record, in FreeSpec.Core.Interface]
Provide3 [record, in FreeSpec.Core.Interface]
Provide4 [record, in FreeSpec.Core.Interface]
Provide5 [record, in FreeSpec.Core.Interface]
ptr:4 [binder, in FreeSpec.Example.heap]
Put [constructor, in FreeSpec.Core.Interface]
put_o_callee [constructor, in FreeSpec.Core.Contract]
P1:351 [binder, in FreeSpec.Core.Interface]
P1:357 [binder, in FreeSpec.Core.Interface]
P1:363 [binder, in FreeSpec.Core.Interface]
P1:370 [binder, in FreeSpec.Core.Interface]
P1:377 [binder, in FreeSpec.Core.Interface]
P1:385 [binder, in FreeSpec.Core.Interface]
p:10 [binder, in FreeSpec.Core.Component]
p:102 [binder, in FreeSpec.Example.smram]
p:104 [binder, in FreeSpec.Example.airlock]
p:106 [binder, in FreeSpec.Example.smram]
p:109 [binder, in FreeSpec.Core.SemanticsFacts]
p:12 [binder, in FreeSpec.Core.Impure]
p:132 [binder, in FreeSpec.Core.SemanticsFacts]
p:138 [binder, in FreeSpec.Core.SemanticsFacts]
p:144 [binder, in FreeSpec.Core.SemanticsFacts]
p:16 [binder, in FreeSpec.Core.InstrumentFacts]
p:19 [binder, in FreeSpec.Core.Component]
p:21 [binder, in FreeSpec.Core.Impure]
p:25 [binder, in FreeSpec.Core.InstrumentFacts]
p:27 [binder, in FreeSpec.Core.ImpureFacts]
p:30 [binder, in FreeSpec.Core.Component]
p:30 [binder, in FreeSpec.Core.Impure]
p:33 [binder, in FreeSpec.Core.ImpureFacts]
p:35 [binder, in FreeSpec.Core.InstrumentFacts]
p:43 [binder, in FreeSpec.Core.HoareFacts]
p:5 [binder, in FreeSpec.Core.Init]
p:51 [binder, in FreeSpec.Core.Semantics]
p:52 [binder, in FreeSpec.Core.Impure]
p:55 [binder, in FreeSpec.Core.Semantics]
p:59 [binder, in FreeSpec.Core.Semantics]
p:59 [binder, in FreeSpec.Core.HoareFacts]
p:64 [binder, in FreeSpec.Core.Semantics]
p:7 [binder, in FreeSpec.Core.ComponentFacts]
p:7 [binder, in FreeSpec.Core.InstrumentFacts]
p:74 [binder, in FreeSpec.Core.Semantics]
p:80 [binder, in FreeSpec.Core.HoareFacts]
p:88 [binder, in FreeSpec.Example.smram]

Q

q:31 [binder, in FreeSpec.Core.Impure]

R

Read [constructor, in FreeSpec.Example.smram]
ReadFrom [constructor, in FreeSpec.Example.smram]
read_in_smram [constructor, in FreeSpec.Example.smram]
reference [axiom, in FreeSpec.FFI.Refs]
refl_Distinguish [instance, in FreeSpec.Core.Interface]
refl_Provide [instance, in FreeSpec.Core.Interface]
refl_MayProvide [instance, in FreeSpec.Core.Interface]
REFS [inductive, in FreeSpec.FFI.Refs]
Refs [library]
reg:69 [binder, in FreeSpec.Example.smram]
request [definition, in FreeSpec.Core.Impure]
RequestOpen [constructor, in FreeSpec.Example.airlock]
request_then_Proper [instance, in FreeSpec.Core.ImpureFacts]
request_eq [constructor, in FreeSpec.Core.ImpureFacts]
request_open [definition, in FreeSpec.Example.airlock]
request_then [constructor, in FreeSpec.Core.Impure]
req_toggle [constructor, in FreeSpec.Example.airlock]
req_is_open [constructor, in FreeSpec.Example.airlock]
respectful_run_inv [lemma, in FreeSpec.Example.airlock]
res_eq:52 [binder, in FreeSpec.Core.SemanticsFacts]
res:11 [binder, in FreeSpec.Core.Component]
res:22 [binder, in FreeSpec.Core.Component]
res:31 [binder, in FreeSpec.Core.Component]
res:67 [binder, in FreeSpec.Core.Semantics]
right [constructor, in FreeSpec.Example.airlock]
run_impure [definition, in FreeSpec.Core.Semantics]
run_effect_equation [lemma, in FreeSpec.Core.Semantics]
run_effect [definition, in FreeSpec.Core.Semantics]
run_impure_Proper_2 [instance, in FreeSpec.Core.SemanticsFacts]
run_impure_Proper_1 [instance, in FreeSpec.Core.SemanticsFacts]
run_impure_bind_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
run_impure_request_then_assoc [lemma, in FreeSpec.Core.SemanticsFacts]
run_impure_equation [lemma, in FreeSpec.Core.SemanticsFacts]
run_effect_Proper [instance, in FreeSpec.Core.SemanticsFacts]
run_effect_Equivalence [instance, in FreeSpec.Core.SemanticsFacts]
run_effect_eq [definition, in FreeSpec.Core.SemanticsFacts]
run:30 [binder, in FreeSpec.Core.ComponentFacts]
run:50 [binder, in FreeSpec.Core.HoareFacts]
run:95 [binder, in FreeSpec.Example.airlock]
r:14 [binder, in FreeSpec.Core.Init]
r:9 [binder, in FreeSpec.Core.Init]
r:99 [binder, in FreeSpec.Example.smram]

S

safe:106 [binder, in FreeSpec.Example.airlock]
safe:87 [binder, in FreeSpec.Example.airlock]
safe:98 [binder, in FreeSpec.Example.airlock]
sel [definition, in FreeSpec.Example.airlock]
semantics [inductive, in FreeSpec.Core.Semantics]
Semantics [library]
SemanticsFacts [library]
semantics_Equivalence [instance, in FreeSpec.Core.SemanticsFacts]
semantics_eq_rec [constructor, in FreeSpec.Core.SemanticsFacts]
semantics_eq [inductive, in FreeSpec.Core.SemanticsFacts]
semi:76 [binder, in FreeSpec.Core.SemanticsFacts]
semi:82 [binder, in FreeSpec.Core.SemanticsFacts]
semi:88 [binder, in FreeSpec.Core.SemanticsFacts]
semi:94 [binder, in FreeSpec.Core.SemanticsFacts]
semj:78 [binder, in FreeSpec.Core.SemanticsFacts]
semj:84 [binder, in FreeSpec.Core.SemanticsFacts]
semj:90 [binder, in FreeSpec.Core.SemanticsFacts]
semj:96 [binder, in FreeSpec.Core.SemanticsFacts]
semprod [definition, in FreeSpec.Core.Semantics]
semprod_Proper [instance, in FreeSpec.Core.SemanticsFacts]
sem_j:35 [binder, in FreeSpec.Core.Semantics]
sem_i:34 [binder, in FreeSpec.Core.Semantics]
sem':49 [binder, in FreeSpec.Core.SemanticsFacts]
sem:108 [binder, in FreeSpec.Core.SemanticsFacts]
sem:11 [binder, in FreeSpec.Core.ComponentFacts]
sem:113 [binder, in FreeSpec.Core.SemanticsFacts]
sem:119 [binder, in FreeSpec.Core.SemanticsFacts]
sem:125 [binder, in FreeSpec.Core.SemanticsFacts]
sem:131 [binder, in FreeSpec.Core.SemanticsFacts]
sem:137 [binder, in FreeSpec.Core.SemanticsFacts]
sem:143 [binder, in FreeSpec.Core.SemanticsFacts]
sem:153 [binder, in FreeSpec.Example.smram]
sem:17 [binder, in FreeSpec.Core.Semantics]
sem:18 [binder, in FreeSpec.Core.InstrumentFacts]
sem:22 [binder, in FreeSpec.Core.Semantics]
sem:26 [binder, in FreeSpec.Core.Semantics]
sem:27 [binder, in FreeSpec.Core.SemanticsFacts]
sem:27 [binder, in FreeSpec.Core.InstrumentFacts]
sem:30 [binder, in FreeSpec.Core.Semantics]
sem:37 [binder, in FreeSpec.Core.InstrumentFacts]
sem:38 [binder, in FreeSpec.Core.SemanticsFacts]
sem:4 [binder, in FreeSpec.Core.ComponentFacts]
sem:43 [binder, in FreeSpec.Core.SemanticsFacts]
sem:45 [binder, in FreeSpec.Core.ComponentFacts]
sem:46 [binder, in FreeSpec.Core.Semantics]
sem:48 [binder, in FreeSpec.Core.SemanticsFacts]
sem:50 [binder, in FreeSpec.Core.Semantics]
sem:54 [binder, in FreeSpec.Core.Semantics]
sem:58 [binder, in FreeSpec.Core.Semantics]
sem:63 [binder, in FreeSpec.Core.Semantics]
sem:7 [binder, in FreeSpec.Core.Component]
sem:8 [binder, in FreeSpec.Core.SemanticsFacts]
sem:9 [binder, in FreeSpec.Core.InstrumentFacts]
smiact [inductive, in FreeSpec.Example.smram]
smiact_unset [constructor, in FreeSpec.Example.smram]
smiact_set [constructor, in FreeSpec.Example.smram]
smram [library]
smram_pred [definition, in FreeSpec.Example.smram]
snd_Proper [instance, in FreeSpec.Core.SemanticsFacts]
step [definition, in FreeSpec.Example.airlock]
step:36 [binder, in FreeSpec.Core.HoareFacts]
store [definition, in FreeSpec.Core.Semantics]
STORE [inductive, in FreeSpec.Core.Interface]
store_specs [definition, in FreeSpec.Core.Contract]
store_update [definition, in FreeSpec.Core.Contract]
store_complies_to_store_specs [lemma, in FreeSpec.Core.SemanticsFacts]
store_monad_state [instance, in FreeSpec.Core.Impure]
StrictProvide2 [record, in FreeSpec.Core.Interface]
StrictProvide3 [record, in FreeSpec.Core.Interface]
StrictProvide4 [record, in FreeSpec.Core.Interface]
StrictProvide5 [record, in FreeSpec.Core.Interface]
st:17 [binder, in FreeSpec.Core.SemanticsFacts]
s'':19 [binder, in FreeSpec.Core.Hoare]
s':11 [binder, in FreeSpec.Core.Hoare]
s':11 [binder, in FreeSpec.Core.HoareFacts]
s':21 [binder, in FreeSpec.Core.Hoare]
s':24 [binder, in FreeSpec.Core.Hoare]
s:102 [binder, in FreeSpec.Core.Contract]
s:16 [binder, in FreeSpec.Core.SemanticsFacts]
s:17 [binder, in FreeSpec.Core.Hoare]
s:22 [binder, in FreeSpec.Core.Hoare]
s:3 [binder, in FreeSpec.Core.Interface]
s:42 [binder, in FreeSpec.Core.Impure]
s:7 [binder, in FreeSpec.Core.HoareFacts]
s:71 [binder, in FreeSpec.Core.Semantics]
s:88 [binder, in FreeSpec.Core.Contract]
s:9 [binder, in FreeSpec.Core.Hoare]
s:9 [binder, in FreeSpec.Core.Semantics]
s:9 [binder, in FreeSpec.Core.HoareFacts]
s:93 [binder, in FreeSpec.Core.Contract]

T

Tactics [library]
tick [definition, in FreeSpec.Example.airlock]
Tick [constructor, in FreeSpec.Example.airlock]
tog [definition, in FreeSpec.Example.airlock]
toggle [definition, in FreeSpec.Example.airlock]
Toggle [constructor, in FreeSpec.Example.airlock]
tog_equ_2 [lemma, in FreeSpec.Example.airlock]
tog_equ_1 [lemma, in FreeSpec.Example.airlock]
to_hoare [definition, in FreeSpec.Core.Hoare]
to_state [definition, in FreeSpec.Core.Semantics]
to_instrument [definition, in FreeSpec.Core.Instrument]
to_hoare_contractprod [lemma, in FreeSpec.Core.HoareFacts]
to_hoare_post_bind_assoc [lemma, in FreeSpec.Core.HoareFacts]
to_hoare_pre_bind_assoc [lemma, in FreeSpec.Core.HoareFacts]
to_hoare_step [lemma, in FreeSpec.Core.HoareFacts]
to_hoare_Proper [instance, in FreeSpec.Core.HoareFacts]

U

unpriv:67 [binder, in FreeSpec.Example.smram]
unwrap_sumbool [definition, in FreeSpec.Example.smram]
update_memory_controller_view [definition, in FreeSpec.Example.smram]
update_dram_view [definition, in FreeSpec.Example.smram]
update_memory_view_address [definition, in FreeSpec.Example.smram]
u:101 [binder, in FreeSpec.Core.Contract]
u:14 [binder, in FreeSpec.Core.Contract]
u:44 [binder, in FreeSpec.Core.SemanticsFacts]

V

value:18 [binder, in FreeSpec.Example.smram]
value:53 [binder, in FreeSpec.Example.smram]
val:31 [binder, in FreeSpec.Example.smram]
val:44 [binder, in FreeSpec.Example.smram]
VGA [inductive, in FreeSpec.Example.smram]
vga_write_to [definition, in FreeSpec.Example.smram]
vga_read_from [definition, in FreeSpec.Example.smram]
v:95 [binder, in FreeSpec.Example.smram]
v:98 [binder, in FreeSpec.Example.smram]

W

when [definition, in FreeSpec.Core.Init]
with_store [definition, in FreeSpec.Core.Semantics]
with_semantics [definition, in FreeSpec.Core.Semantics]
with_component [definition, in FreeSpec.Core.Component]
with_component_aux [definition, in FreeSpec.Core.Component]
with_heap_impure [definition, in FreeSpec.Example.heap]
with_heap [definition, in FreeSpec.Example.heap]
witness_update [projection, in FreeSpec.Core.Contract]
write [constructor, in FreeSpec.Example.smram]
Write [constructor, in FreeSpec.Example.smram]
WriteTo [constructor, in FreeSpec.Example.smram]

X

x':100 [binder, in FreeSpec.Core.Contract]
x':98 [binder, in FreeSpec.Core.Contract]
x0:25 [binder, in FreeSpec.FFI.Refs]
x0:29 [binder, in FreeSpec.FFI.Refs]
x0:33 [binder, in FreeSpec.FFI.Refs]
x1:34 [binder, in FreeSpec.FFI.Refs]
x:10 [binder, in FreeSpec.Core.HoareFacts]
x:107 [binder, in FreeSpec.Example.smram]
x:107 [binder, in FreeSpec.Example.airlock]
x:12 [binder, in FreeSpec.Core.Init]
x:16 [binder, in FreeSpec.Core.Impure]
x:17 [binder, in FreeSpec.Core.Contract]
x:18 [binder, in FreeSpec.Core.Hoare]
x:22 [binder, in FreeSpec.Core.Impure]
x:23 [binder, in FreeSpec.Core.Hoare]
x:23 [binder, in FreeSpec.Core.Component]
x:26 [binder, in FreeSpec.Core.Impure]
x:28 [binder, in FreeSpec.Core.ComponentFacts]
x:28 [binder, in FreeSpec.Core.ImpureFacts]
x:30 [binder, in FreeSpec.Core.Hoare]
x:30 [binder, in FreeSpec.Core.Contract]
x:35 [binder, in FreeSpec.Core.HoareFacts]
x:36 [binder, in FreeSpec.Core.ImpureFacts]
x:39 [binder, in FreeSpec.Core.Semantics]
x:4 [binder, in FreeSpec.Exec.Eval]
x:41 [binder, in FreeSpec.Core.Semantics]
x:41 [binder, in FreeSpec.Core.Impure]
x:44 [binder, in FreeSpec.Core.ImpureFacts]
x:46 [binder, in FreeSpec.Core.Impure]
x:48 [binder, in FreeSpec.Core.Hoare]
x:48 [binder, in FreeSpec.Core.Contract]
x:48 [binder, in FreeSpec.Core.HoareFacts]
x:5 [binder, in FreeSpec.Core.ImpureFacts]
x:5 [binder, in FreeSpec.Core.Impure]
x:5 [binder, in FreeSpec.Example.heap]
x:51 [binder, in FreeSpec.Core.HoareFacts]
x:52 [binder, in FreeSpec.Core.HoareFacts]
x:55 [binder, in FreeSpec.Core.Impure]
x:56 [binder, in FreeSpec.Example.smram]
x:57 [binder, in FreeSpec.Example.airlock]
x:59 [binder, in FreeSpec.Core.SemanticsFacts]
x:6 [binder, in FreeSpec.Core.Interface]
x:63 [binder, in FreeSpec.Core.HoareFacts]
x:65 [binder, in FreeSpec.Core.Contract]
x:69 [binder, in FreeSpec.Core.Semantics]
x:72 [binder, in FreeSpec.Example.airlock]
x:73 [binder, in FreeSpec.Core.Semantics]
x:76 [binder, in FreeSpec.Example.airlock]
x:8 [binder, in FreeSpec.Core.Hoare]
x:8 [binder, in FreeSpec.Core.Instrument]
x:80 [binder, in FreeSpec.Core.Contract]
x:80 [binder, in FreeSpec.Example.smram]
x:81 [binder, in FreeSpec.Example.smram]
x:87 [binder, in FreeSpec.Core.Contract]
x:89 [binder, in FreeSpec.Core.Contract]
x:9 [binder, in FreeSpec.Exec.Eval]
x:94 [binder, in FreeSpec.Core.Contract]
x:94 [binder, in FreeSpec.Example.airlock]

Y

y:10 [binder, in FreeSpec.Core.Hoare]
y:20 [binder, in FreeSpec.Core.Hoare]
y:60 [binder, in FreeSpec.Core.SemanticsFacts]
y:66 [binder, in FreeSpec.Core.HoareFacts]

other

_ * _ (contract_scope) [notation, in FreeSpec.Core.Contract]
_ === _ (impure_scope) [notation, in FreeSpec.Core.ImpureFacts]
_ + _ (interface_scope) [notation, in FreeSpec.Core.Interface]
_ * _ (semantics_scope) [notation, in FreeSpec.Core.Semantics]
_ === _ (semantics_scope) [notation, in FreeSpec.Core.SemanticsFacts]
_ ~> _ (type_scope) [notation, in FreeSpec.Core.Init]
Σ:1 [binder, in FreeSpec.Core.Hoare]
Σ:1 [binder, in FreeSpec.Core.HoareFacts]
Σ:12 [binder, in FreeSpec.Core.Hoare]
Σ:25 [binder, in FreeSpec.Core.Hoare]
Σ:31 [binder, in FreeSpec.Core.Hoare]
Σ:32 [binder, in FreeSpec.Core.Hoare]
Σ:39 [binder, in FreeSpec.Core.Hoare]
Σ:6 [binder, in FreeSpec.Core.Hoare]
Ω [definition, in FreeSpec.Example.airlock]
Ωi:17 [binder, in FreeSpec.Core.ComponentFacts]
Ωi:36 [binder, in FreeSpec.Core.ComponentFacts]
Ωi:73 [binder, in FreeSpec.Core.Contract]
Ωi:75 [binder, in FreeSpec.Core.HoareFacts]
Ωj:19 [binder, in FreeSpec.Core.ComponentFacts]
Ωj:38 [binder, in FreeSpec.Core.ComponentFacts]
Ωj:74 [binder, in FreeSpec.Core.Contract]
Ωj:77 [binder, in FreeSpec.Core.HoareFacts]
Ω:104 [binder, in FreeSpec.Core.SemanticsFacts]
Ω:13 [binder, in FreeSpec.Core.Instrument]
Ω:13 [binder, in FreeSpec.Core.InstrumentFacts]
Ω:16 [binder, in FreeSpec.Core.Instrument]
Ω:19 [binder, in FreeSpec.Core.Contract]
Ω:2 [binder, in FreeSpec.Core.Contract]
Ω:21 [binder, in FreeSpec.Core.SemanticsFacts]
Ω:22 [binder, in FreeSpec.Core.InstrumentFacts]
Ω:26 [binder, in FreeSpec.Core.Contract]
Ω:28 [binder, in FreeSpec.Core.HoareFacts]
Ω:32 [binder, in FreeSpec.Core.SemanticsFacts]
Ω:32 [binder, in FreeSpec.Core.InstrumentFacts]
Ω:35 [binder, in FreeSpec.Core.Contract]
Ω:4 [binder, in FreeSpec.Core.Instrument]
Ω:4 [binder, in FreeSpec.Core.SemanticsFacts]
Ω:4 [binder, in FreeSpec.Core.InstrumentFacts]
Ω:40 [binder, in FreeSpec.Core.HoareFacts]
Ω:43 [binder, in FreeSpec.Core.Hoare]
Ω:43 [binder, in FreeSpec.Core.Contract]
Ω:52 [binder, in FreeSpec.Core.Contract]
Ω:54 [binder, in FreeSpec.Core.Hoare]
Ω:56 [binder, in FreeSpec.Core.HoareFacts]
Ω:60 [binder, in FreeSpec.Core.Contract]
α:10 [binder, in FreeSpec.Core.SemanticsFacts]
α:10 [binder, in FreeSpec.Core.Impure]
α:10 [binder, in FreeSpec.Core.Interface]
α:11 [binder, in FreeSpec.Core.Contract]
α:12 [binder, in FreeSpec.Core.Semantics]
α:13 [binder, in FreeSpec.Core.Hoare]
α:13 [binder, in FreeSpec.Core.SemanticsFacts]
α:15 [binder, in FreeSpec.Core.Contract]
α:16 [binder, in FreeSpec.Core.Semantics]
α:17 [binder, in FreeSpec.Core.Component]
α:17 [binder, in FreeSpec.Core.Interface]
α:18 [binder, in FreeSpec.Core.Impure]
α:2 [binder, in FreeSpec.Core.Hoare]
α:2 [binder, in FreeSpec.Core.ImpureFacts]
α:2 [binder, in FreeSpec.Core.HoareFacts]
α:2 [binder, in FreeSpec.Core.Impure]
α:20 [binder, in FreeSpec.Core.Interface]
α:21 [binder, in FreeSpec.Core.Contract]
α:21 [binder, in FreeSpec.Core.Semantics]
α:24 [binder, in FreeSpec.Core.SemanticsFacts]
α:25 [binder, in FreeSpec.Core.ComponentFacts]
α:25 [binder, in FreeSpec.Core.Semantics]
α:25 [binder, in FreeSpec.Core.Impure]
α:26 [binder, in FreeSpec.Core.Hoare]
α:26 [binder, in FreeSpec.Core.ImpureFacts]
α:26 [binder, in FreeSpec.Core.Component]
α:28 [binder, in FreeSpec.Core.Contract]
α:28 [binder, in FreeSpec.Core.Impure]
α:29 [binder, in FreeSpec.Core.Semantics]
α:3 [binder, in FreeSpec.Core.Component]
α:30 [binder, in FreeSpec.Core.ImpureFacts]
α:309 [binder, in FreeSpec.Core.Interface]
α:32 [binder, in FreeSpec.Core.Interface]
α:33 [binder, in FreeSpec.Core.Hoare]
α:33 [binder, in FreeSpec.Core.SemanticsFacts]
α:37 [binder, in FreeSpec.Core.Contract]
α:39 [binder, in FreeSpec.Core.Impure]
α:4 [binder, in FreeSpec.Core.Semantics]
α:44 [binder, in FreeSpec.Core.Contract]
α:5 [binder, in FreeSpec.Core.Contract]
α:53 [binder, in FreeSpec.Core.Contract]
α:57 [binder, in FreeSpec.Core.SemanticsFacts]
α:6 [binder, in FreeSpec.Core.Semantics]
α:6 [binder, in FreeSpec.Core.Init]
α:61 [binder, in FreeSpec.Core.Contract]
α:62 [binder, in FreeSpec.Core.Semantics]
α:7 [binder, in FreeSpec.Core.Hoare]
α:78 [binder, in FreeSpec.Core.Contract]
α:79 [binder, in FreeSpec.Core.SemanticsFacts]
α:8 [binder, in FreeSpec.Core.Contract]
α:82 [binder, in FreeSpec.Core.Contract]
α:85 [binder, in FreeSpec.Core.Contract]
α:85 [binder, in FreeSpec.Core.SemanticsFacts]
α:90 [binder, in FreeSpec.Core.Contract]
α:91 [binder, in FreeSpec.Core.SemanticsFacts]
α:95 [binder, in FreeSpec.Core.Contract]
α:97 [binder, in FreeSpec.Core.SemanticsFacts]
β:11 [binder, in FreeSpec.Core.Impure]
β:14 [binder, in FreeSpec.Core.Hoare]
β:19 [binder, in FreeSpec.Core.Impure]
β:27 [binder, in FreeSpec.Core.Hoare]
β:29 [binder, in FreeSpec.Core.Impure]
β:31 [binder, in FreeSpec.Core.ImpureFacts]
β:34 [binder, in FreeSpec.Core.Hoare]
β:6 [binder, in FreeSpec.Core.ImpureFacts]
β:6 [binder, in FreeSpec.Core.Impure]
δ:32 [binder, in FreeSpec.Core.ImpureFacts]
ωi:22 [binder, in FreeSpec.Core.ComponentFacts]
ωi:42 [binder, in FreeSpec.Core.ComponentFacts]
ωi:81 [binder, in FreeSpec.Core.HoareFacts]
ωj':29 [binder, in FreeSpec.Core.ComponentFacts]
ωj:23 [binder, in FreeSpec.Core.ComponentFacts]
ωj:43 [binder, in FreeSpec.Core.ComponentFacts]
ωj:83 [binder, in FreeSpec.Core.HoareFacts]
ωmc:118 [binder, in FreeSpec.Example.smram]
ωmem:119 [binder, in FreeSpec.Example.smram]
ω'':67 [binder, in FreeSpec.Core.HoareFacts]
ω':108 [binder, in FreeSpec.Example.airlock]
ω':49 [binder, in FreeSpec.Core.Hoare]
ω':49 [binder, in FreeSpec.Core.HoareFacts]
ω':64 [binder, in FreeSpec.Core.HoareFacts]
ω':93 [binder, in FreeSpec.Example.airlock]
ω:10 [binder, in FreeSpec.Core.Contract]
ω:100 [binder, in FreeSpec.Example.smram]
ω:104 [binder, in FreeSpec.Example.smram]
ω:105 [binder, in FreeSpec.Example.airlock]
ω:119 [binder, in FreeSpec.Example.airlock]
ω:137 [binder, in FreeSpec.Example.smram]
ω:152 [binder, in FreeSpec.Example.smram]
ω:17 [binder, in FreeSpec.Core.Instrument]
ω:17 [binder, in FreeSpec.Core.InstrumentFacts]
ω:20 [binder, in FreeSpec.Core.Contract]
ω:23 [binder, in FreeSpec.Core.SemanticsFacts]
ω:26 [binder, in FreeSpec.Core.InstrumentFacts]
ω:27 [binder, in FreeSpec.Core.Contract]
ω:33 [binder, in FreeSpec.Core.HoareFacts]
ω:35 [binder, in FreeSpec.Core.SemanticsFacts]
ω:36 [binder, in FreeSpec.Core.Contract]
ω:36 [binder, in FreeSpec.Core.InstrumentFacts]
ω:4 [binder, in FreeSpec.Core.Contract]
ω:44 [binder, in FreeSpec.Core.HoareFacts]
ω:46 [binder, in FreeSpec.Core.Contract]
ω:47 [binder, in FreeSpec.Core.Hoare]
ω:48 [binder, in FreeSpec.Example.airlock]
ω:50 [binder, in FreeSpec.Core.Hoare]
ω:51 [binder, in FreeSpec.Example.airlock]
ω:53 [binder, in FreeSpec.Example.airlock]
ω:54 [binder, in FreeSpec.Example.airlock]
ω:55 [binder, in FreeSpec.Core.Contract]
ω:62 [binder, in FreeSpec.Core.HoareFacts]
ω:63 [binder, in FreeSpec.Core.Contract]
ω:63 [binder, in FreeSpec.Example.airlock]
ω:65 [binder, in FreeSpec.Example.airlock]
ω:7 [binder, in FreeSpec.Core.Contract]
ω:71 [binder, in FreeSpec.Example.airlock]
ω:75 [binder, in FreeSpec.Example.airlock]
ω:77 [binder, in FreeSpec.Core.Contract]
ω:8 [binder, in FreeSpec.Core.InstrumentFacts]
ω:80 [binder, in FreeSpec.Example.airlock]
ω:81 [binder, in FreeSpec.Core.Contract]
ω:82 [binder, in FreeSpec.Example.smram]
ω:84 [binder, in FreeSpec.Core.Contract]
ω:85 [binder, in FreeSpec.Example.airlock]
ω:86 [binder, in FreeSpec.Example.smram]
ω:9 [binder, in FreeSpec.Core.Instrument]
ω:9 [binder, in FreeSpec.Core.SemanticsFacts]
ω:90 [binder, in FreeSpec.Example.smram]
ω:91 [binder, in FreeSpec.Example.airlock]
ω:96 [binder, in FreeSpec.Example.airlock]

Notation Index

other

_ * _ (contract_scope) [in FreeSpec.Core.Contract]
_ === _ (impure_scope) [in FreeSpec.Core.ImpureFacts]
_ + _ (interface_scope) [in FreeSpec.Core.Interface]
_ * _ (semantics_scope) [in FreeSpec.Core.Semantics]
_ === _ (semantics_scope) [in FreeSpec.Core.SemanticsFacts]
_ ~> _ (type_scope) [in FreeSpec.Core.Init]

Binder Index

A

addr':12 [in FreeSpec.Example.smram]
addr':5 [in FreeSpec.Example.smram]
addr':8 [in FreeSpec.Example.smram]
addr':85 [in FreeSpec.Example.smram]
addr:11 [in FreeSpec.Example.smram]
addr:111 [in FreeSpec.Example.smram]
addr:115 [in FreeSpec.Example.smram]
addr:16 [in FreeSpec.Example.smram]
addr:17 [in FreeSpec.Example.smram]
addr:26 [in FreeSpec.Example.smram]
addr:30 [in FreeSpec.Example.smram]
addr:39 [in FreeSpec.Example.smram]
addr:4 [in FreeSpec.Example.smram]
addr:43 [in FreeSpec.Example.smram]
addr:50 [in FreeSpec.Example.smram]
addr:52 [in FreeSpec.Example.smram]
addr:66 [in FreeSpec.Example.smram]
addr:7 [in FreeSpec.Example.smram]
addr:83 [in FreeSpec.Example.smram]
a:1 [in FreeSpec.Exec.Eval]
a:1 [in FreeSpec.FFI.Refs]
a:101 [in FreeSpec.Example.smram]
a:103 [in FreeSpec.Example.airlock]
a:105 [in FreeSpec.Example.smram]
a:107 [in FreeSpec.Core.SemanticsFacts]
a:11 [in FreeSpec.FFI.Refs]
a:111 [in FreeSpec.Core.SemanticsFacts]
a:117 [in FreeSpec.Core.SemanticsFacts]
a:120 [in FreeSpec.Example.smram]
a:123 [in FreeSpec.Core.SemanticsFacts]
a:129 [in FreeSpec.Core.SemanticsFacts]
a:13 [in FreeSpec.FFI.Refs]
a:135 [in FreeSpec.Example.smram]
a:135 [in FreeSpec.Core.SemanticsFacts]
a:141 [in FreeSpec.Core.SemanticsFacts]
a:147 [in FreeSpec.Core.SemanticsFacts]
a:149 [in FreeSpec.Core.SemanticsFacts]
a:15 [in FreeSpec.FFI.Refs]
a:15 [in FreeSpec.Core.InstrumentFacts]
a:151 [in FreeSpec.Core.SemanticsFacts]
a:153 [in FreeSpec.Core.SemanticsFacts]
a:18 [in FreeSpec.Core.Instrument]
a:19 [in FreeSpec.FFI.Refs]
a:20 [in FreeSpec.FFI.Refs]
a:21 [in FreeSpec.Example.smram]
a:21 [in FreeSpec.FFI.Refs]
a:24 [in FreeSpec.FFI.Refs]
a:24 [in FreeSpec.Core.InstrumentFacts]
a:28 [in FreeSpec.FFI.Refs]
a:30 [in FreeSpec.Core.HoareFacts]
a:317 [in FreeSpec.Core.Interface]
a:32 [in FreeSpec.FFI.Refs]
a:330 [in FreeSpec.Core.Interface]
a:34 [in FreeSpec.Example.smram]
a:34 [in FreeSpec.Core.InstrumentFacts]
a:38 [in FreeSpec.Core.ImpureFacts]
a:4 [in FreeSpec.Core.Init]
a:42 [in FreeSpec.Core.HoareFacts]
a:44 [in FreeSpec.Core.Semantics]
a:45 [in FreeSpec.Core.Hoare]
a:49 [in FreeSpec.Core.Semantics]
a:5 [in FreeSpec.FFI.Refs]
a:50 [in FreeSpec.Core.SemanticsFacts]
a:51 [in FreeSpec.Core.Impure]
a:53 [in FreeSpec.Core.Semantics]
a:53 [in FreeSpec.Core.SemanticsFacts]
A:54 [in FreeSpec.Example.smram]
a:55 [in FreeSpec.Example.airlock]
a:57 [in FreeSpec.Core.Semantics]
a:57 [in FreeSpec.Example.smram]
a:58 [in FreeSpec.Core.HoareFacts]
a:59 [in FreeSpec.Example.airlock]
a:6 [in FreeSpec.Core.ComponentFacts]
a:6 [in FreeSpec.Core.Instrument]
a:6 [in FreeSpec.Core.InstrumentFacts]
a:67 [in FreeSpec.Example.airlock]
a:7 [in FreeSpec.FFI.Refs]
a:7 [in FreeSpec.Core.Init]
a:72 [in FreeSpec.Core.Semantics]
a:79 [in FreeSpec.Core.HoareFacts]
a:8 [in FreeSpec.Exec.Eval]
a:87 [in FreeSpec.Example.smram]
a:9 [in FreeSpec.Core.Component]
a:9 [in FreeSpec.FFI.Refs]
a:91 [in FreeSpec.Example.smram]
a:94 [in FreeSpec.Example.smram]
a:97 [in FreeSpec.Example.smram]

B

b:112 [in FreeSpec.Core.SemanticsFacts]
b:117 [in FreeSpec.Example.smram]
b:118 [in FreeSpec.Core.SemanticsFacts]
b:124 [in FreeSpec.Core.SemanticsFacts]
b:13 [in FreeSpec.Core.Init]
b:130 [in FreeSpec.Core.SemanticsFacts]
b:136 [in FreeSpec.Core.SemanticsFacts]
b:142 [in FreeSpec.Core.SemanticsFacts]
b:40 [in FreeSpec.Core.ImpureFacts]
b:46 [in FreeSpec.Core.HoareFacts]
B:55 [in FreeSpec.Example.smram]
b:60 [in FreeSpec.Core.HoareFacts]
b:8 [in FreeSpec.Core.Init]

C

ci:18 [in FreeSpec.Core.ComponentFacts]
ci:37 [in FreeSpec.Core.ComponentFacts]
ci:75 [in FreeSpec.Core.Contract]
ci:76 [in FreeSpec.Core.HoareFacts]
cj:20 [in FreeSpec.Core.ComponentFacts]
cj:39 [in FreeSpec.Core.ComponentFacts]
cj:76 [in FreeSpec.Core.Contract]
cj:78 [in FreeSpec.Core.HoareFacts]
comp:154 [in FreeSpec.Example.smram]
comp:28 [in FreeSpec.Core.SemanticsFacts]
comp:28 [in FreeSpec.Core.InstrumentFacts]
comp:38 [in FreeSpec.Core.InstrumentFacts]
comp:39 [in FreeSpec.Core.SemanticsFacts]
comp:46 [in FreeSpec.Core.ComponentFacts]
cond:3 [in FreeSpec.Core.Init]
content:112 [in FreeSpec.Example.smram]
content:116 [in FreeSpec.Example.smram]
content:84 [in FreeSpec.Example.smram]
correct:41 [in FreeSpec.Core.ComponentFacts]
cpt:44 [in FreeSpec.Example.airlock]
c:10 [in FreeSpec.Core.ComponentFacts]
c:105 [in FreeSpec.Core.SemanticsFacts]
c:14 [in FreeSpec.Core.Instrument]
c:14 [in FreeSpec.Core.Component]
c:14 [in FreeSpec.Core.InstrumentFacts]
c:16 [in FreeSpec.Core.ComponentFacts]
c:18 [in FreeSpec.Core.Component]
c:22 [in FreeSpec.Core.SemanticsFacts]
c:23 [in FreeSpec.Core.InstrumentFacts]
c:28 [in FreeSpec.Core.Component]
c:29 [in FreeSpec.Core.HoareFacts]
c:3 [in FreeSpec.Core.ComponentFacts]
c:33 [in FreeSpec.Core.InstrumentFacts]
c:34 [in FreeSpec.Core.SemanticsFacts]
c:35 [in FreeSpec.Core.ComponentFacts]
c:41 [in FreeSpec.Core.HoareFacts]
c:42 [in FreeSpec.Core.ImpureFacts]
c:44 [in FreeSpec.Core.Hoare]
c:45 [in FreeSpec.Core.Contract]
c:5 [in FreeSpec.Core.Instrument]
c:5 [in FreeSpec.Core.SemanticsFacts]
c:5 [in FreeSpec.Core.InstrumentFacts]
c:54 [in FreeSpec.Core.Contract]
c:55 [in FreeSpec.Core.Hoare]
c:57 [in FreeSpec.Core.HoareFacts]
c:6 [in FreeSpec.Core.Component]
c:62 [in FreeSpec.Core.Contract]

D

Distinguish0:138 [in FreeSpec.Core.Interface]
Distinguish0:148 [in FreeSpec.Core.Interface]
Distinguish0:160 [in FreeSpec.Core.Interface]
Distinguish0:177 [in FreeSpec.Core.Interface]
Distinguish0:196 [in FreeSpec.Core.Interface]
Distinguish0:222 [in FreeSpec.Core.Interface]
Distinguish0:250 [in FreeSpec.Core.Interface]
Distinguish0:287 [in FreeSpec.Core.Interface]
Distinguish10:206 [in FreeSpec.Core.Interface]
Distinguish10:232 [in FreeSpec.Core.Interface]
Distinguish10:260 [in FreeSpec.Core.Interface]
Distinguish10:297 [in FreeSpec.Core.Interface]
Distinguish11:207 [in FreeSpec.Core.Interface]
Distinguish11:233 [in FreeSpec.Core.Interface]
Distinguish11:261 [in FreeSpec.Core.Interface]
Distinguish11:298 [in FreeSpec.Core.Interface]
Distinguish12:262 [in FreeSpec.Core.Interface]
Distinguish12:299 [in FreeSpec.Core.Interface]
Distinguish13:263 [in FreeSpec.Core.Interface]
Distinguish13:300 [in FreeSpec.Core.Interface]
Distinguish14:264 [in FreeSpec.Core.Interface]
Distinguish14:301 [in FreeSpec.Core.Interface]
Distinguish15:265 [in FreeSpec.Core.Interface]
Distinguish15:302 [in FreeSpec.Core.Interface]
Distinguish16:266 [in FreeSpec.Core.Interface]
Distinguish16:303 [in FreeSpec.Core.Interface]
Distinguish17:267 [in FreeSpec.Core.Interface]
Distinguish17:304 [in FreeSpec.Core.Interface]
Distinguish18:268 [in FreeSpec.Core.Interface]
Distinguish18:305 [in FreeSpec.Core.Interface]
Distinguish19:269 [in FreeSpec.Core.Interface]
Distinguish19:306 [in FreeSpec.Core.Interface]
Distinguish1:139 [in FreeSpec.Core.Interface]
Distinguish1:149 [in FreeSpec.Core.Interface]
Distinguish1:161 [in FreeSpec.Core.Interface]
Distinguish1:178 [in FreeSpec.Core.Interface]
Distinguish1:197 [in FreeSpec.Core.Interface]
Distinguish1:223 [in FreeSpec.Core.Interface]
Distinguish1:251 [in FreeSpec.Core.Interface]
Distinguish1:288 [in FreeSpec.Core.Interface]
Distinguish2:162 [in FreeSpec.Core.Interface]
Distinguish2:179 [in FreeSpec.Core.Interface]
Distinguish2:198 [in FreeSpec.Core.Interface]
Distinguish2:224 [in FreeSpec.Core.Interface]
Distinguish2:252 [in FreeSpec.Core.Interface]
Distinguish2:289 [in FreeSpec.Core.Interface]
Distinguish3:163 [in FreeSpec.Core.Interface]
Distinguish3:180 [in FreeSpec.Core.Interface]
Distinguish3:199 [in FreeSpec.Core.Interface]
Distinguish3:225 [in FreeSpec.Core.Interface]
Distinguish3:253 [in FreeSpec.Core.Interface]
Distinguish3:290 [in FreeSpec.Core.Interface]
Distinguish4:164 [in FreeSpec.Core.Interface]
Distinguish4:181 [in FreeSpec.Core.Interface]
Distinguish4:200 [in FreeSpec.Core.Interface]
Distinguish4:226 [in FreeSpec.Core.Interface]
Distinguish4:254 [in FreeSpec.Core.Interface]
Distinguish4:291 [in FreeSpec.Core.Interface]
Distinguish5:165 [in FreeSpec.Core.Interface]
Distinguish5:182 [in FreeSpec.Core.Interface]
Distinguish5:201 [in FreeSpec.Core.Interface]
Distinguish5:227 [in FreeSpec.Core.Interface]
Distinguish5:255 [in FreeSpec.Core.Interface]
Distinguish5:292 [in FreeSpec.Core.Interface]
Distinguish6:202 [in FreeSpec.Core.Interface]
Distinguish6:228 [in FreeSpec.Core.Interface]
Distinguish6:256 [in FreeSpec.Core.Interface]
Distinguish6:293 [in FreeSpec.Core.Interface]
Distinguish7:203 [in FreeSpec.Core.Interface]
Distinguish7:229 [in FreeSpec.Core.Interface]
Distinguish7:257 [in FreeSpec.Core.Interface]
Distinguish7:294 [in FreeSpec.Core.Interface]
Distinguish8:204 [in FreeSpec.Core.Interface]
Distinguish8:230 [in FreeSpec.Core.Interface]
Distinguish8:258 [in FreeSpec.Core.Interface]
Distinguish8:295 [in FreeSpec.Core.Interface]
Distinguish9:205 [in FreeSpec.Core.Interface]
Distinguish9:231 [in FreeSpec.Core.Interface]
Distinguish9:259 [in FreeSpec.Core.Interface]
Distinguish9:296 [in FreeSpec.Core.Interface]
d':4 [in FreeSpec.Example.airlock]
d':99 [in FreeSpec.Example.airlock]
d:10 [in FreeSpec.Example.airlock]
d:14 [in FreeSpec.Example.airlock]
d:18 [in FreeSpec.Example.airlock]
d:23 [in FreeSpec.Example.airlock]
d:27 [in FreeSpec.Example.airlock]
d:3 [in FreeSpec.Example.airlock]
d:34 [in FreeSpec.Example.airlock]
d:35 [in FreeSpec.Example.airlock]
d:45 [in FreeSpec.Example.airlock]
d:47 [in FreeSpec.Example.airlock]
d:50 [in FreeSpec.Example.airlock]
d:52 [in FreeSpec.Example.airlock]
d:62 [in FreeSpec.Example.airlock]
d:64 [in FreeSpec.Example.airlock]
d:70 [in FreeSpec.Example.airlock]
d:74 [in FreeSpec.Example.airlock]
d:81 [in FreeSpec.Example.airlock]
d:86 [in FreeSpec.Example.airlock]
d:92 [in FreeSpec.Example.airlock]
d:97 [in FreeSpec.Example.airlock]

E

equ:10 [in FreeSpec.Core.ImpureFacts]
equ:73 [in FreeSpec.Example.airlock]
equ:99 [in FreeSpec.Core.Contract]
e:11 [in FreeSpec.Core.SemanticsFacts]
e:11 [in FreeSpec.Core.Interface]
e:114 [in FreeSpec.Core.SemanticsFacts]
e:120 [in FreeSpec.Core.SemanticsFacts]
e:126 [in FreeSpec.Core.SemanticsFacts]
e:13 [in FreeSpec.Core.Semantics]
e:14 [in FreeSpec.Core.SemanticsFacts]
e:16 [in FreeSpec.Core.Contract]
e:18 [in FreeSpec.Core.Semantics]
e:18 [in FreeSpec.Core.Interface]
e:21 [in FreeSpec.Core.Interface]
e:22 [in FreeSpec.Core.Contract]
e:22 [in FreeSpec.Example.smram]
e:23 [in FreeSpec.Core.Semantics]
e:25 [in FreeSpec.Core.SemanticsFacts]
e:26 [in FreeSpec.Core.ComponentFacts]
e:27 [in FreeSpec.Core.Semantics]
e:29 [in FreeSpec.Core.Contract]
e:31 [in FreeSpec.Core.Semantics]
e:31 [in FreeSpec.Core.HoareFacts]
e:312 [in FreeSpec.Core.Interface]
e:313 [in FreeSpec.Core.Interface]
e:315 [in FreeSpec.Core.Interface]
e:318 [in FreeSpec.Core.Interface]
e:323 [in FreeSpec.Core.Interface]
e:33 [in FreeSpec.Core.Interface]
e:331 [in FreeSpec.Core.Interface]
e:336 [in FreeSpec.Core.Interface]
e:343 [in FreeSpec.Core.Interface]
e:35 [in FreeSpec.Example.smram]
e:36 [in FreeSpec.Core.SemanticsFacts]
e:37 [in FreeSpec.Core.Semantics]
e:38 [in FreeSpec.Core.Contract]
e:39 [in FreeSpec.Core.ImpureFacts]
e:40 [in FreeSpec.Core.Impure]
e:45 [in FreeSpec.Core.Semantics]
e:46 [in FreeSpec.Core.Hoare]
e:47 [in FreeSpec.Core.Contract]
e:51 [in FreeSpec.Core.SemanticsFacts]
e:54 [in FreeSpec.Core.SemanticsFacts]
e:56 [in FreeSpec.Core.Contract]
e:56 [in FreeSpec.Example.airlock]
e:64 [in FreeSpec.Core.Contract]
e:7 [in FreeSpec.Core.ImpureFacts]
e:7 [in FreeSpec.Core.Semantics]
e:7 [in FreeSpec.Core.Instrument]
e:7 [in FreeSpec.Core.Impure]
e:79 [in FreeSpec.Core.Contract]
e:80 [in FreeSpec.Core.SemanticsFacts]
e:83 [in FreeSpec.Core.Contract]
e:86 [in FreeSpec.Core.Contract]
e:86 [in FreeSpec.Core.SemanticsFacts]
e:91 [in FreeSpec.Core.Contract]
e:92 [in FreeSpec.Core.SemanticsFacts]
e:98 [in FreeSpec.Core.SemanticsFacts]

F

finalizer:29 [in FreeSpec.Core.Component]
f:10 [in FreeSpec.Core.Init]
f:115 [in FreeSpec.Core.SemanticsFacts]
f:121 [in FreeSpec.Core.SemanticsFacts]
f:127 [in FreeSpec.Core.SemanticsFacts]
f:13 [in FreeSpec.Core.Impure]
f:133 [in FreeSpec.Core.SemanticsFacts]
f:139 [in FreeSpec.Core.SemanticsFacts]
f:145 [in FreeSpec.Core.SemanticsFacts]
f:20 [in FreeSpec.Core.Impure]
f:28 [in FreeSpec.Core.Hoare]
f:32 [in FreeSpec.Core.HoareFacts]
f:32 [in FreeSpec.Core.Impure]
f:34 [in FreeSpec.Core.ImpureFacts]
f:37 [in FreeSpec.Core.Hoare]
f:41 [in FreeSpec.Core.ImpureFacts]
f:47 [in FreeSpec.Core.HoareFacts]
f:5 [in FreeSpec.Core.Semantics]
f:61 [in FreeSpec.Core.HoareFacts]
f:8 [in FreeSpec.Core.ImpureFacts]
f:8 [in FreeSpec.Core.Impure]

G

g:11 [in FreeSpec.Core.Init]
g:35 [in FreeSpec.Core.ImpureFacts]
g:43 [in FreeSpec.Core.ImpureFacts]
g:9 [in FreeSpec.Core.ImpureFacts]

H

hf:35 [in FreeSpec.Core.Hoare]
hpost:110 [in FreeSpec.Example.airlock]
hpre:109 [in FreeSpec.Example.airlock]
hpre:34 [in FreeSpec.Core.HoareFacts]
Hp:45 [in FreeSpec.Core.HoareFacts]
Hp:65 [in FreeSpec.Core.HoareFacts]
H0:102 [in FreeSpec.Example.airlock]
H0:105 [in FreeSpec.Core.Interface]
H0:118 [in FreeSpec.Core.Interface]
H0:13 [in FreeSpec.Example.airlock]
H0:135 [in FreeSpec.Core.Interface]
H0:144 [in FreeSpec.Core.Interface]
H0:155 [in FreeSpec.Core.Interface]
H0:17 [in FreeSpec.Example.airlock]
H0:170 [in FreeSpec.Core.Interface]
H0:189 [in FreeSpec.Core.Interface]
H0:212 [in FreeSpec.Core.Interface]
H0:22 [in FreeSpec.Example.airlock]
H0:241 [in FreeSpec.Core.Interface]
H0:25 [in FreeSpec.Example.smram]
H0:278 [in FreeSpec.Core.Interface]
H0:29 [in FreeSpec.Example.smram]
H0:29 [in FreeSpec.Core.Interface]
H0:3 [in FreeSpec.Example.heap]
H0:30 [in FreeSpec.Example.airlock]
H0:329 [in FreeSpec.Core.Interface]
H0:33 [in FreeSpec.Example.airlock]
H0:342 [in FreeSpec.Core.Interface]
H0:38 [in FreeSpec.Example.smram]
H0:38 [in FreeSpec.Core.Impure]
H0:39 [in FreeSpec.Example.airlock]
H0:39 [in FreeSpec.Core.Interface]
H0:42 [in FreeSpec.Example.smram]
H0:45 [in FreeSpec.Core.Impure]
H0:46 [in FreeSpec.Core.Interface]
H0:55 [in FreeSpec.Core.Interface]
H0:64 [in FreeSpec.Core.Interface]
H0:69 [in FreeSpec.Core.Contract]
H0:7 [in FreeSpec.Exec.Eval]
H0:71 [in FreeSpec.Core.HoareFacts]
H0:77 [in FreeSpec.Core.Interface]
H0:79 [in FreeSpec.Example.airlock]
H0:8 [in FreeSpec.Example.heap]
H0:84 [in FreeSpec.Example.airlock]
H0:88 [in FreeSpec.Core.Interface]
H0:9 [in FreeSpec.Example.airlock]
H0:90 [in FreeSpec.Example.airlock]
h1:3 [in FreeSpec.Core.HoareFacts]
H1:30 [in FreeSpec.Core.Interface]
H2:107 [in FreeSpec.Core.Interface]
H2:121 [in FreeSpec.Core.Interface]
H2:137 [in FreeSpec.Core.Interface]
H2:147 [in FreeSpec.Core.Interface]
H2:157 [in FreeSpec.Core.Interface]
H2:173 [in FreeSpec.Core.Interface]
H2:191 [in FreeSpec.Core.Interface]
H2:215 [in FreeSpec.Core.Interface]
H2:243 [in FreeSpec.Core.Interface]
H2:280 [in FreeSpec.Core.Interface]
h2:4 [in FreeSpec.Core.HoareFacts]
H2:41 [in FreeSpec.Example.airlock]
H2:41 [in FreeSpec.Core.Interface]
H2:49 [in FreeSpec.Core.Interface]
H2:57 [in FreeSpec.Core.Interface]
H2:67 [in FreeSpec.Core.Interface]
H2:72 [in FreeSpec.Core.Contract]
H2:74 [in FreeSpec.Core.HoareFacts]
H2:79 [in FreeSpec.Core.Interface]
H2:91 [in FreeSpec.Core.Interface]
H3:118 [in FreeSpec.Example.airlock]
H4:109 [in FreeSpec.Core.Interface]
H4:124 [in FreeSpec.Core.Interface]
H4:159 [in FreeSpec.Core.Interface]
H4:176 [in FreeSpec.Core.Interface]
H4:193 [in FreeSpec.Core.Interface]
H4:218 [in FreeSpec.Core.Interface]
H4:245 [in FreeSpec.Core.Interface]
H4:282 [in FreeSpec.Core.Interface]
H4:59 [in FreeSpec.Core.Interface]
H4:70 [in FreeSpec.Core.Interface]
H4:81 [in FreeSpec.Core.Interface]
H4:94 [in FreeSpec.Core.Interface]
H5:134 [in FreeSpec.Example.smram]
H5:151 [in FreeSpec.Example.smram]
H5:65 [in FreeSpec.Example.smram]
H5:77 [in FreeSpec.Example.smram]
H6:111 [in FreeSpec.Core.Interface]
H6:127 [in FreeSpec.Core.Interface]
H6:195 [in FreeSpec.Core.Interface]
H6:221 [in FreeSpec.Core.Interface]
H6:247 [in FreeSpec.Core.Interface]
H6:284 [in FreeSpec.Core.Interface]
H6:83 [in FreeSpec.Core.Interface]
H6:97 [in FreeSpec.Core.Interface]
H8:113 [in FreeSpec.Core.Interface]
H8:130 [in FreeSpec.Core.Interface]
H8:249 [in FreeSpec.Core.Interface]
H8:286 [in FreeSpec.Core.Interface]
H:103 [in FreeSpec.Core.SemanticsFacts]
H:12 [in FreeSpec.Core.Instrument]
H:12 [in FreeSpec.Core.InstrumentFacts]
H:14 [in FreeSpec.Core.ComponentFacts]
h:15 [in FreeSpec.Core.Hoare]
H:15 [in FreeSpec.Core.Init]
H:15 [in FreeSpec.Core.Interface]
H:2 [in FreeSpec.Core.Init]
H:2 [in FreeSpec.Example.heap]
H:20 [in FreeSpec.Core.SemanticsFacts]
H:21 [in FreeSpec.Core.InstrumentFacts]
H:23 [in FreeSpec.FFI.Refs]
H:27 [in FreeSpec.Core.HoareFacts]
H:27 [in FreeSpec.FFI.Refs]
h:29 [in FreeSpec.Core.Hoare]
H:3 [in FreeSpec.Core.Instrument]
H:3 [in FreeSpec.Core.SemanticsFacts]
H:3 [in FreeSpec.Core.InstrumentFacts]
H:31 [in FreeSpec.Core.SemanticsFacts]
H:31 [in FreeSpec.FFI.Refs]
H:31 [in FreeSpec.Core.InstrumentFacts]
H:322 [in FreeSpec.Core.Interface]
H:33 [in FreeSpec.Core.ComponentFacts]
H:335 [in FreeSpec.Core.Interface]
h:36 [in FreeSpec.Core.Hoare]
H:36 [in FreeSpec.FFI.Refs]
H:379 [in FreeSpec.Core.Interface]
H:387 [in FreeSpec.Core.Interface]
H:39 [in FreeSpec.Core.HoareFacts]
H:4 [in FreeSpec.FFI.FFI]
H:42 [in FreeSpec.Core.Hoare]
H:42 [in FreeSpec.Core.Contract]
H:42 [in FreeSpec.Core.SemanticsFacts]
H:48 [in FreeSpec.Core.Impure]
H:51 [in FreeSpec.Core.Contract]
H:53 [in FreeSpec.Core.Hoare]
H:55 [in FreeSpec.Core.HoareFacts]
H:59 [in FreeSpec.Core.Contract]
H:66 [in FreeSpec.Example.airlock]

I

initializer:27 [in FreeSpec.Core.Component]
init:10 [in FreeSpec.Core.Semantics]
init:24 [in FreeSpec.Core.ComponentFacts]
instr:19 [in FreeSpec.Core.Instrument]
inv:44 [in FreeSpec.Core.ComponentFacts]
ix:1 [in FreeSpec.FFI.FFI]
ix:1 [in FreeSpec.Core.Instrument]
ix:1 [in FreeSpec.Core.SemanticsFacts]
ix:1 [in FreeSpec.Core.InstrumentFacts]
ix:10 [in FreeSpec.Core.Instrument]
ix:10 [in FreeSpec.Core.InstrumentFacts]
ix:100 [in FreeSpec.Example.airlock]
ix:101 [in FreeSpec.Core.SemanticsFacts]
ix:11 [in FreeSpec.Example.airlock]
ix:111 [in FreeSpec.Example.airlock]
ix:115 [in FreeSpec.Core.Interface]
ix:121 [in FreeSpec.Example.smram]
ix:13 [in FreeSpec.Core.Interface]
ix:131 [in FreeSpec.Core.Interface]
ix:138 [in FreeSpec.Example.smram]
ix:141 [in FreeSpec.Core.Interface]
ix:15 [in FreeSpec.Example.airlock]
ix:15 [in FreeSpec.Core.Component]
ix:150 [in FreeSpec.Core.Interface]
ix:167 [in FreeSpec.Core.Interface]
ix:18 [in FreeSpec.Core.SemanticsFacts]
ix:183 [in FreeSpec.Core.Interface]
ix:19 [in FreeSpec.Core.InstrumentFacts]
ix:20 [in FreeSpec.Example.airlock]
ix:209 [in FreeSpec.Core.Interface]
ix:23 [in FreeSpec.Example.smram]
ix:234 [in FreeSpec.Core.Interface]
ix:24 [in FreeSpec.Core.Component]
ix:25 [in FreeSpec.Core.HoareFacts]
ix:25 [in FreeSpec.Core.Interface]
ix:27 [in FreeSpec.Example.smram]
ix:271 [in FreeSpec.Core.Interface]
ix:28 [in FreeSpec.Example.airlock]
ix:29 [in FreeSpec.Core.SemanticsFacts]
ix:29 [in FreeSpec.Core.InstrumentFacts]
ix:31 [in FreeSpec.Example.airlock]
ix:319 [in FreeSpec.Core.Interface]
ix:325 [in FreeSpec.Core.Interface]
ix:346 [in FreeSpec.Core.Interface]
ix:35 [in FreeSpec.Core.Impure]
ix:35 [in FreeSpec.Core.Interface]
ix:352 [in FreeSpec.Core.Interface]
ix:358 [in FreeSpec.Core.Interface]
ix:36 [in FreeSpec.Example.smram]
ix:365 [in FreeSpec.Core.Interface]
ix:37 [in FreeSpec.Core.HoareFacts]
ix:37 [in FreeSpec.Example.airlock]
ix:372 [in FreeSpec.Core.Interface]
ix:380 [in FreeSpec.Core.Interface]
ix:40 [in FreeSpec.Core.Hoare]
ix:40 [in FreeSpec.Core.Contract]
ix:40 [in FreeSpec.Example.smram]
ix:40 [in FreeSpec.Core.SemanticsFacts]
ix:43 [in FreeSpec.Core.Impure]
ix:43 [in FreeSpec.Core.Interface]
ix:49 [in FreeSpec.Core.Contract]
ix:5 [in FreeSpec.Exec.Eval]
ix:50 [in FreeSpec.Core.Interface]
ix:51 [in FreeSpec.Core.Hoare]
ix:53 [in FreeSpec.Core.HoareFacts]
ix:57 [in FreeSpec.Core.Contract]
ix:58 [in FreeSpec.Example.smram]
ix:6 [in FreeSpec.Example.heap]
ix:60 [in FreeSpec.Core.Semantics]
ix:61 [in FreeSpec.Core.Interface]
ix:66 [in FreeSpec.Core.Contract]
ix:68 [in FreeSpec.Core.HoareFacts]
ix:7 [in FreeSpec.Example.airlock]
ix:7 [in FreeSpec.Core.Interface]
ix:70 [in FreeSpec.Core.Semantics]
ix:70 [in FreeSpec.Example.smram]
ix:71 [in FreeSpec.Core.Interface]
ix:77 [in FreeSpec.Example.airlock]
ix:82 [in FreeSpec.Example.airlock]
ix:85 [in FreeSpec.Core.Interface]
ix:88 [in FreeSpec.Example.airlock]
ix:98 [in FreeSpec.Core.Interface]
i1:116 [in FreeSpec.Core.Interface]
i1:132 [in FreeSpec.Core.Interface]
i1:142 [in FreeSpec.Core.Interface]
i1:151 [in FreeSpec.Core.Interface]
i1:168 [in FreeSpec.Core.Interface]
i1:184 [in FreeSpec.Core.Interface]
i1:210 [in FreeSpec.Core.Interface]
i1:235 [in FreeSpec.Core.Interface]
i1:272 [in FreeSpec.Core.Interface]
i1:36 [in FreeSpec.Core.Interface]
i1:44 [in FreeSpec.Core.Interface]
i1:51 [in FreeSpec.Core.Interface]
i1:62 [in FreeSpec.Core.Interface]
i1:72 [in FreeSpec.Core.Interface]
i1:86 [in FreeSpec.Core.Interface]
i1:99 [in FreeSpec.Core.Interface]
i2:100 [in FreeSpec.Core.Interface]
i2:119 [in FreeSpec.Core.Interface]
i2:133 [in FreeSpec.Core.Interface]
i2:145 [in FreeSpec.Core.Interface]
i2:152 [in FreeSpec.Core.Interface]
i2:171 [in FreeSpec.Core.Interface]
i2:185 [in FreeSpec.Core.Interface]
i2:213 [in FreeSpec.Core.Interface]
i2:236 [in FreeSpec.Core.Interface]
i2:273 [in FreeSpec.Core.Interface]
i2:37 [in FreeSpec.Core.Interface]
i2:47 [in FreeSpec.Core.Interface]
i2:52 [in FreeSpec.Core.Interface]
i2:65 [in FreeSpec.Core.Interface]
i2:73 [in FreeSpec.Core.Interface]
i2:89 [in FreeSpec.Core.Interface]
i3:101 [in FreeSpec.Core.Interface]
i3:122 [in FreeSpec.Core.Interface]
i3:153 [in FreeSpec.Core.Interface]
i3:174 [in FreeSpec.Core.Interface]
i3:186 [in FreeSpec.Core.Interface]
i3:216 [in FreeSpec.Core.Interface]
i3:237 [in FreeSpec.Core.Interface]
i3:274 [in FreeSpec.Core.Interface]
i3:53 [in FreeSpec.Core.Interface]
i3:68 [in FreeSpec.Core.Interface]
i3:74 [in FreeSpec.Core.Interface]
i3:92 [in FreeSpec.Core.Interface]
i4:102 [in FreeSpec.Core.Interface]
i4:125 [in FreeSpec.Core.Interface]
i4:187 [in FreeSpec.Core.Interface]
i4:219 [in FreeSpec.Core.Interface]
i4:238 [in FreeSpec.Core.Interface]
i4:275 [in FreeSpec.Core.Interface]
i4:75 [in FreeSpec.Core.Interface]
i4:95 [in FreeSpec.Core.Interface]
i5:103 [in FreeSpec.Core.Interface]
i5:128 [in FreeSpec.Core.Interface]
i5:239 [in FreeSpec.Core.Interface]
i5:276 [in FreeSpec.Core.Interface]
i:1 [in FreeSpec.Core.ComponentFacts]
i:1 [in FreeSpec.Core.Contract]
i:1 [in FreeSpec.Core.ImpureFacts]
i:1 [in FreeSpec.Core.Semantics]
i:1 [in FreeSpec.Core.Component]
i:1 [in FreeSpec.Core.Impure]
i:102 [in FreeSpec.Core.SemanticsFacts]
i:106 [in FreeSpec.Core.SemanticsFacts]
i:11 [in FreeSpec.Core.Instrument]
i:11 [in FreeSpec.Core.InstrumentFacts]
i:110 [in FreeSpec.Core.SemanticsFacts]
i:116 [in FreeSpec.Core.SemanticsFacts]
i:122 [in FreeSpec.Core.SemanticsFacts]
i:128 [in FreeSpec.Core.SemanticsFacts]
i:13 [in FreeSpec.Core.Contract]
i:13 [in FreeSpec.Core.Component]
i:134 [in FreeSpec.Core.SemanticsFacts]
i:14 [in FreeSpec.Core.Interface]
i:140 [in FreeSpec.Core.SemanticsFacts]
i:146 [in FreeSpec.Core.SemanticsFacts]
i:148 [in FreeSpec.Core.SemanticsFacts]
i:15 [in FreeSpec.Core.ComponentFacts]
i:15 [in FreeSpec.Core.Semantics]
i:15 [in FreeSpec.Core.Instrument]
i:150 [in FreeSpec.Core.SemanticsFacts]
i:152 [in FreeSpec.Core.SemanticsFacts]
i:17 [in FreeSpec.Core.Impure]
i:18 [in FreeSpec.Core.Contract]
i:19 [in FreeSpec.Core.SemanticsFacts]
i:2 [in FreeSpec.FFI.FFI]
i:2 [in FreeSpec.Core.Instrument]
i:2 [in FreeSpec.Core.SemanticsFacts]
i:2 [in FreeSpec.Core.InstrumentFacts]
i:20 [in FreeSpec.Core.Semantics]
i:20 [in FreeSpec.Core.InstrumentFacts]
i:23 [in FreeSpec.Core.Interface]
i:24 [in FreeSpec.Core.Semantics]
i:24 [in FreeSpec.Core.Impure]
i:25 [in FreeSpec.Core.Contract]
i:25 [in FreeSpec.Core.ImpureFacts]
i:26 [in FreeSpec.Core.HoareFacts]
i:26 [in FreeSpec.Core.Interface]
i:27 [in FreeSpec.Core.Impure]
i:28 [in FreeSpec.Core.Semantics]
i:29 [in FreeSpec.Core.ImpureFacts]
i:30 [in FreeSpec.Core.SemanticsFacts]
i:30 [in FreeSpec.Core.InstrumentFacts]
i:307 [in FreeSpec.Core.Interface]
i:314 [in FreeSpec.Core.Interface]
i:316 [in FreeSpec.Core.Interface]
i:32 [in FreeSpec.Core.Semantics]
i:320 [in FreeSpec.Core.Interface]
i:326 [in FreeSpec.Core.Interface]
i:33 [in FreeSpec.Core.Contract]
i:332 [in FreeSpec.Core.Interface]
i:338 [in FreeSpec.Core.Interface]
i:34 [in FreeSpec.Core.ComponentFacts]
i:34 [in FreeSpec.Core.Contract]
i:34 [in FreeSpec.Core.Impure]
i:344 [in FreeSpec.Core.Interface]
i:348 [in FreeSpec.Core.Interface]
i:354 [in FreeSpec.Core.Interface]
i:36 [in FreeSpec.Core.Impure]
i:360 [in FreeSpec.Core.Interface]
i:367 [in FreeSpec.Core.Interface]
i:37 [in FreeSpec.Core.ImpureFacts]
i:374 [in FreeSpec.Core.Interface]
i:38 [in FreeSpec.Core.HoareFacts]
i:382 [in FreeSpec.Core.Interface]
i:39 [in FreeSpec.Core.Contract]
i:4 [in FreeSpec.Core.Component]
i:41 [in FreeSpec.Core.Hoare]
i:41 [in FreeSpec.Core.Contract]
i:41 [in FreeSpec.Core.SemanticsFacts]
i:43 [in FreeSpec.Core.Semantics]
i:45 [in FreeSpec.Core.SemanticsFacts]
i:47 [in FreeSpec.Core.Semantics]
i:48 [in FreeSpec.Core.Semantics]
i:49 [in FreeSpec.Core.Impure]
i:50 [in FreeSpec.Core.Contract]
i:52 [in FreeSpec.Core.Hoare]
i:52 [in FreeSpec.Core.Semantics]
i:54 [in FreeSpec.Core.HoareFacts]
i:56 [in FreeSpec.Core.Semantics]
i:56 [in FreeSpec.Core.SemanticsFacts]
i:58 [in FreeSpec.Core.Contract]
i:58 [in FreeSpec.Core.SemanticsFacts]
i:67 [in FreeSpec.Core.Contract]
i:69 [in FreeSpec.Core.HoareFacts]
i:75 [in FreeSpec.Core.SemanticsFacts]
i:8 [in FreeSpec.Core.ComponentFacts]
i:8 [in FreeSpec.Core.Interface]
i:81 [in FreeSpec.Core.SemanticsFacts]
i:87 [in FreeSpec.Core.SemanticsFacts]
i:9 [in FreeSpec.Core.Impure]
i:93 [in FreeSpec.Core.SemanticsFacts]
i:99 [in FreeSpec.Core.SemanticsFacts]

J

jx:12 [in FreeSpec.Core.ComponentFacts]
jx:31 [in FreeSpec.Core.ComponentFacts]
jx:333 [in FreeSpec.Core.Interface]
jx:339 [in FreeSpec.Core.Interface]
jx:347 [in FreeSpec.Core.Interface]
jx:353 [in FreeSpec.Core.Interface]
jx:359 [in FreeSpec.Core.Interface]
jx:366 [in FreeSpec.Core.Interface]
jx:373 [in FreeSpec.Core.Interface]
jx:381 [in FreeSpec.Core.Interface]
j:100 [in FreeSpec.Core.SemanticsFacts]
j:13 [in FreeSpec.Core.ComponentFacts]
j:16 [in FreeSpec.Core.Component]
j:2 [in FreeSpec.Core.ComponentFacts]
j:2 [in FreeSpec.Core.Component]
j:24 [in FreeSpec.Core.Interface]
j:25 [in FreeSpec.Core.Component]
j:27 [in FreeSpec.Core.Interface]
j:308 [in FreeSpec.Core.Interface]
j:32 [in FreeSpec.Core.ComponentFacts]
j:321 [in FreeSpec.Core.Interface]
j:327 [in FreeSpec.Core.Interface]
j:33 [in FreeSpec.Core.Semantics]
j:334 [in FreeSpec.Core.Interface]
j:340 [in FreeSpec.Core.Interface]
j:345 [in FreeSpec.Core.Interface]
j:349 [in FreeSpec.Core.Interface]
j:355 [in FreeSpec.Core.Interface]
j:361 [in FreeSpec.Core.Interface]
j:368 [in FreeSpec.Core.Interface]
j:375 [in FreeSpec.Core.Interface]
j:383 [in FreeSpec.Core.Interface]
j:5 [in FreeSpec.Core.Component]
j:61 [in FreeSpec.Core.Semantics]
j:70 [in FreeSpec.Core.Contract]
j:72 [in FreeSpec.Core.HoareFacts]
j:77 [in FreeSpec.Core.SemanticsFacts]
j:83 [in FreeSpec.Core.SemanticsFacts]
j:89 [in FreeSpec.Core.SemanticsFacts]
j:9 [in FreeSpec.Core.ComponentFacts]
j:95 [in FreeSpec.Core.SemanticsFacts]

K

k:16 [in FreeSpec.Core.Hoare]

L

l:50 [in FreeSpec.Core.Impure]

M

M1:350 [in FreeSpec.Core.Interface]
M1:356 [in FreeSpec.Core.Interface]
M1:362 [in FreeSpec.Core.Interface]
M1:369 [in FreeSpec.Core.Interface]
M1:376 [in FreeSpec.Core.Interface]
M1:384 [in FreeSpec.Core.Interface]
M2:364 [in FreeSpec.Core.Interface]
M2:371 [in FreeSpec.Core.Interface]
M2:378 [in FreeSpec.Core.Interface]
M2:386 [in FreeSpec.Core.Interface]
m:1 [in FreeSpec.Core.Init]
m:1 [in FreeSpec.Example.heap]
m:22 [in FreeSpec.FFI.Refs]
m:26 [in FreeSpec.FFI.Refs]
m:3 [in FreeSpec.FFI.Refs]
m:30 [in FreeSpec.FFI.Refs]
m:35 [in FreeSpec.FFI.Refs]
m:47 [in FreeSpec.Core.Impure]

N

next_eq:55 [in FreeSpec.Core.SemanticsFacts]
next:12 [in FreeSpec.Core.Component]
next:15 [in FreeSpec.Core.SemanticsFacts]
next:68 [in FreeSpec.Core.Semantics]

O

open:19 [in FreeSpec.Example.airlock]
open:24 [in FreeSpec.Example.airlock]
op:136 [in FreeSpec.Example.smram]
op:42 [in FreeSpec.Example.airlock]
op:78 [in FreeSpec.Example.smram]
out:40 [in FreeSpec.Core.Semantics]
out:42 [in FreeSpec.Core.Semantics]
o_caller:27 [in FreeSpec.Core.ComponentFacts]
o_caller:37 [in FreeSpec.Core.SemanticsFacts]
o_caller:26 [in FreeSpec.Core.SemanticsFacts]
o_callee:12 [in FreeSpec.Core.SemanticsFacts]

P

pin:110 [in FreeSpec.Example.smram]
pin:114 [in FreeSpec.Example.smram]
pin:49 [in FreeSpec.Example.smram]
pin:51 [in FreeSpec.Example.smram]
post_eq:12 [in FreeSpec.Core.HoareFacts]
pred:21 [in FreeSpec.Core.ComponentFacts]
pred:40 [in FreeSpec.Core.ComponentFacts]
prei:82 [in FreeSpec.Core.HoareFacts]
prej:84 [in FreeSpec.Core.HoareFacts]
pre_eq:8 [in FreeSpec.Core.HoareFacts]
priv:68 [in FreeSpec.Example.smram]
prom:113 [in FreeSpec.Example.smram]
prom:96 [in FreeSpec.Example.smram]
ptr:4 [in FreeSpec.Example.heap]
P1:351 [in FreeSpec.Core.Interface]
P1:357 [in FreeSpec.Core.Interface]
P1:363 [in FreeSpec.Core.Interface]
P1:370 [in FreeSpec.Core.Interface]
P1:377 [in FreeSpec.Core.Interface]
P1:385 [in FreeSpec.Core.Interface]
p:10 [in FreeSpec.Core.Component]
p:102 [in FreeSpec.Example.smram]
p:104 [in FreeSpec.Example.airlock]
p:106 [in FreeSpec.Example.smram]
p:109 [in FreeSpec.Core.SemanticsFacts]
p:12 [in FreeSpec.Core.Impure]
p:132 [in FreeSpec.Core.SemanticsFacts]
p:138 [in FreeSpec.Core.SemanticsFacts]
p:144 [in FreeSpec.Core.SemanticsFacts]
p:16 [in FreeSpec.Core.InstrumentFacts]
p:19 [in FreeSpec.Core.Component]
p:21 [in FreeSpec.Core.Impure]
p:25 [in FreeSpec.Core.InstrumentFacts]
p:27 [in FreeSpec.Core.ImpureFacts]
p:30 [in FreeSpec.Core.Component]
p:30 [in FreeSpec.Core.Impure]
p:33 [in FreeSpec.Core.ImpureFacts]
p:35 [in FreeSpec.Core.InstrumentFacts]
p:43 [in FreeSpec.Core.HoareFacts]
p:5 [in FreeSpec.Core.Init]
p:51 [in FreeSpec.Core.Semantics]
p:52 [in FreeSpec.Core.Impure]
p:55 [in FreeSpec.Core.Semantics]
p:59 [in FreeSpec.Core.Semantics]
p:59 [in FreeSpec.Core.HoareFacts]
p:64 [in FreeSpec.Core.Semantics]
p:7 [in FreeSpec.Core.ComponentFacts]
p:7 [in FreeSpec.Core.InstrumentFacts]
p:74 [in FreeSpec.Core.Semantics]
p:80 [in FreeSpec.Core.HoareFacts]
p:88 [in FreeSpec.Example.smram]

Q

q:31 [in FreeSpec.Core.Impure]

R

reg:69 [in FreeSpec.Example.smram]
res_eq:52 [in FreeSpec.Core.SemanticsFacts]
res:11 [in FreeSpec.Core.Component]
res:22 [in FreeSpec.Core.Component]
res:31 [in FreeSpec.Core.Component]
res:67 [in FreeSpec.Core.Semantics]
run:30 [in FreeSpec.Core.ComponentFacts]
run:50 [in FreeSpec.Core.HoareFacts]
run:95 [in FreeSpec.Example.airlock]
r:14 [in FreeSpec.Core.Init]
r:9 [in FreeSpec.Core.Init]
r:99 [in FreeSpec.Example.smram]

S

safe:106 [in FreeSpec.Example.airlock]
safe:87 [in FreeSpec.Example.airlock]
safe:98 [in FreeSpec.Example.airlock]
semi:76 [in FreeSpec.Core.SemanticsFacts]
semi:82 [in FreeSpec.Core.SemanticsFacts]
semi:88 [in FreeSpec.Core.SemanticsFacts]
semi:94 [in FreeSpec.Core.SemanticsFacts]
semj:78 [in FreeSpec.Core.SemanticsFacts]
semj:84 [in FreeSpec.Core.SemanticsFacts]
semj:90 [in FreeSpec.Core.SemanticsFacts]
semj:96 [in FreeSpec.Core.SemanticsFacts]
sem_j:35 [in FreeSpec.Core.Semantics]
sem_i:34 [in FreeSpec.Core.Semantics]
sem':49 [in FreeSpec.Core.SemanticsFacts]
sem:108 [in FreeSpec.Core.SemanticsFacts]
sem:11 [in FreeSpec.Core.ComponentFacts]
sem:113 [in FreeSpec.Core.SemanticsFacts]
sem:119 [in FreeSpec.Core.SemanticsFacts]
sem:125 [in FreeSpec.Core.SemanticsFacts]
sem:131 [in FreeSpec.Core.SemanticsFacts]
sem:137 [in FreeSpec.Core.SemanticsFacts]
sem:143 [in FreeSpec.Core.SemanticsFacts]
sem:153 [in FreeSpec.Example.smram]
sem:17 [in FreeSpec.Core.Semantics]
sem:18 [in FreeSpec.Core.InstrumentFacts]
sem:22 [in FreeSpec.Core.Semantics]
sem:26 [in FreeSpec.Core.Semantics]
sem:27 [in FreeSpec.Core.SemanticsFacts]
sem:27 [in FreeSpec.Core.InstrumentFacts]
sem:30 [in FreeSpec.Core.Semantics]
sem:37 [in FreeSpec.Core.InstrumentFacts]
sem:38 [in FreeSpec.Core.SemanticsFacts]
sem:4 [in FreeSpec.Core.ComponentFacts]
sem:43 [in FreeSpec.Core.SemanticsFacts]
sem:45 [in FreeSpec.Core.ComponentFacts]
sem:46 [in FreeSpec.Core.Semantics]
sem:48 [in FreeSpec.Core.SemanticsFacts]
sem:50 [in FreeSpec.Core.Semantics]
sem:54 [in FreeSpec.Core.Semantics]
sem:58 [in FreeSpec.Core.Semantics]
sem:63 [in FreeSpec.Core.Semantics]
sem:7 [in FreeSpec.Core.Component]
sem:8 [in FreeSpec.Core.SemanticsFacts]
sem:9 [in FreeSpec.Core.InstrumentFacts]
step:36 [in FreeSpec.Core.HoareFacts]
st:17 [in FreeSpec.Core.SemanticsFacts]
s'':19 [in FreeSpec.Core.Hoare]
s':11 [in FreeSpec.Core.Hoare]
s':11 [in FreeSpec.Core.HoareFacts]
s':21 [in FreeSpec.Core.Hoare]
s':24 [in FreeSpec.Core.Hoare]
s:102 [in FreeSpec.Core.Contract]
s:16 [in FreeSpec.Core.SemanticsFacts]
s:17 [in FreeSpec.Core.Hoare]
s:22 [in FreeSpec.Core.Hoare]
s:3 [in FreeSpec.Core.Interface]
s:42 [in FreeSpec.Core.Impure]
s:7 [in FreeSpec.Core.HoareFacts]
s:71 [in FreeSpec.Core.Semantics]
s:88 [in FreeSpec.Core.Contract]
s:9 [in FreeSpec.Core.Hoare]
s:9 [in FreeSpec.Core.Semantics]
s:9 [in FreeSpec.Core.HoareFacts]
s:93 [in FreeSpec.Core.Contract]

U

unpriv:67 [in FreeSpec.Example.smram]
u:101 [in FreeSpec.Core.Contract]
u:14 [in FreeSpec.Core.Contract]
u:44 [in FreeSpec.Core.SemanticsFacts]

V

value:18 [in FreeSpec.Example.smram]
value:53 [in FreeSpec.Example.smram]
val:31 [in FreeSpec.Example.smram]
val:44 [in FreeSpec.Example.smram]
v:95 [in FreeSpec.Example.smram]
v:98 [in FreeSpec.Example.smram]

X

x':100 [in FreeSpec.Core.Contract]
x':98 [in FreeSpec.Core.Contract]
x0:25 [in FreeSpec.FFI.Refs]
x0:29 [in FreeSpec.FFI.Refs]
x0:33 [in FreeSpec.FFI.Refs]
x1:34 [in FreeSpec.FFI.Refs]
x:10 [in FreeSpec.Core.HoareFacts]
x:107 [in FreeSpec.Example.smram]
x:107 [in FreeSpec.Example.airlock]
x:12 [in FreeSpec.Core.Init]
x:16 [in FreeSpec.Core.Impure]
x:17 [in FreeSpec.Core.Contract]
x:18 [in FreeSpec.Core.Hoare]
x:22 [in FreeSpec.Core.Impure]
x:23 [in FreeSpec.Core.Hoare]
x:23 [in FreeSpec.Core.Component]
x:26 [in FreeSpec.Core.Impure]
x:28 [in FreeSpec.Core.ComponentFacts]
x:28 [in FreeSpec.Core.ImpureFacts]
x:30 [in FreeSpec.Core.Hoare]
x:30 [in FreeSpec.Core.Contract]
x:35 [in FreeSpec.Core.HoareFacts]
x:36 [in FreeSpec.Core.ImpureFacts]
x:39 [in FreeSpec.Core.Semantics]
x:4 [in FreeSpec.Exec.Eval]
x:41 [in FreeSpec.Core.Semantics]
x:41 [in FreeSpec.Core.Impure]
x:44 [in FreeSpec.Core.ImpureFacts]
x:46 [in FreeSpec.Core.Impure]
x:48 [in FreeSpec.Core.Hoare]
x:48 [in FreeSpec.Core.Contract]
x:48 [in FreeSpec.Core.HoareFacts]
x:5 [in FreeSpec.Core.ImpureFacts]
x:5 [in FreeSpec.Core.Impure]
x:5 [in FreeSpec.Example.heap]
x:51 [in FreeSpec.Core.HoareFacts]
x:52 [in FreeSpec.Core.HoareFacts]
x:55 [in FreeSpec.Core.Impure]
x:56 [in FreeSpec.Example.smram]
x:57 [in FreeSpec.Example.airlock]
x:59 [in FreeSpec.Core.SemanticsFacts]
x:6 [in FreeSpec.Core.Interface]
x:63 [in FreeSpec.Core.HoareFacts]
x:65 [in FreeSpec.Core.Contract]
x:69 [in FreeSpec.Core.Semantics]
x:72 [in FreeSpec.Example.airlock]
x:73 [in FreeSpec.Core.Semantics]
x:76 [in FreeSpec.Example.airlock]
x:8 [in FreeSpec.Core.Hoare]
x:8 [in FreeSpec.Core.Instrument]
x:80 [in FreeSpec.Core.Contract]
x:80 [in FreeSpec.Example.smram]
x:81 [in FreeSpec.Example.smram]
x:87 [in FreeSpec.Core.Contract]
x:89 [in FreeSpec.Core.Contract]
x:9 [in FreeSpec.Exec.Eval]
x:94 [in FreeSpec.Core.Contract]
x:94 [in FreeSpec.Example.airlock]

Y

y:10 [in FreeSpec.Core.Hoare]
y:20 [in FreeSpec.Core.Hoare]
y:60 [in FreeSpec.Core.SemanticsFacts]
y:66 [in FreeSpec.Core.HoareFacts]

other

Σ:1 [in FreeSpec.Core.Hoare]
Σ:1 [in FreeSpec.Core.HoareFacts]
Σ:12 [in FreeSpec.Core.Hoare]
Σ:25 [in FreeSpec.Core.Hoare]
Σ:31 [in FreeSpec.Core.Hoare]
Σ:32 [in FreeSpec.Core.Hoare]
Σ:39 [in FreeSpec.Core.Hoare]
Σ:6 [in FreeSpec.Core.Hoare]
Ωi:17 [in FreeSpec.Core.ComponentFacts]
Ωi:36 [in FreeSpec.Core.ComponentFacts]
Ωi:73 [in FreeSpec.Core.Contract]
Ωi:75 [in FreeSpec.Core.HoareFacts]
Ωj:19 [in FreeSpec.Core.ComponentFacts]
Ωj:38 [in FreeSpec.Core.ComponentFacts]
Ωj:74 [in FreeSpec.Core.Contract]
Ωj:77 [in FreeSpec.Core.HoareFacts]
Ω:104 [in FreeSpec.Core.SemanticsFacts]
Ω:13 [in FreeSpec.Core.Instrument]
Ω:13 [in FreeSpec.Core.InstrumentFacts]
Ω:16 [in FreeSpec.Core.Instrument]
Ω:19 [in FreeSpec.Core.Contract]
Ω:2 [in FreeSpec.Core.Contract]
Ω:21 [in FreeSpec.Core.SemanticsFacts]
Ω:22 [in FreeSpec.Core.InstrumentFacts]
Ω:26 [in FreeSpec.Core.Contract]
Ω:28 [in FreeSpec.Core.HoareFacts]
Ω:32 [in FreeSpec.Core.SemanticsFacts]
Ω:32 [in FreeSpec.Core.InstrumentFacts]
Ω:35 [in FreeSpec.Core.Contract]
Ω:4 [in FreeSpec.Core.Instrument]
Ω:4 [in FreeSpec.Core.SemanticsFacts]
Ω:4 [in FreeSpec.Core.InstrumentFacts]
Ω:40 [in FreeSpec.Core.HoareFacts]
Ω:43 [in FreeSpec.Core.Hoare]
Ω:43 [in FreeSpec.Core.Contract]
Ω:52 [in FreeSpec.Core.Contract]
Ω:54 [in FreeSpec.Core.Hoare]
Ω:56 [in FreeSpec.Core.HoareFacts]
Ω:60 [in FreeSpec.Core.Contract]
α:10 [in FreeSpec.Core.SemanticsFacts]
α:10 [in FreeSpec.Core.Impure]
α:10 [in FreeSpec.Core.Interface]
α:11 [in FreeSpec.Core.Contract]
α:12 [in FreeSpec.Core.Semantics]
α:13 [in FreeSpec.Core.Hoare]
α:13 [in FreeSpec.Core.SemanticsFacts]
α:15 [in FreeSpec.Core.Contract]
α:16 [in FreeSpec.Core.Semantics]
α:17 [in FreeSpec.Core.Component]
α:17 [in FreeSpec.Core.Interface]
α:18 [in FreeSpec.Core.Impure]
α:2 [in FreeSpec.Core.Hoare]
α:2 [in FreeSpec.Core.ImpureFacts]
α:2 [in FreeSpec.Core.HoareFacts]
α:2 [in FreeSpec.Core.Impure]
α:20 [in FreeSpec.Core.Interface]
α:21 [in FreeSpec.Core.Contract]
α:21 [in FreeSpec.Core.Semantics]
α:24 [in FreeSpec.Core.SemanticsFacts]
α:25 [in FreeSpec.Core.ComponentFacts]
α:25 [in FreeSpec.Core.Semantics]
α:25 [in FreeSpec.Core.Impure]
α:26 [in FreeSpec.Core.Hoare]
α:26 [in FreeSpec.Core.ImpureFacts]
α:26 [in FreeSpec.Core.Component]
α:28 [in FreeSpec.Core.Contract]
α:28 [in FreeSpec.Core.Impure]
α:29 [in FreeSpec.Core.Semantics]
α:3 [in FreeSpec.Core.Component]
α:30 [in FreeSpec.Core.ImpureFacts]
α:309 [in FreeSpec.Core.Interface]
α:32 [in FreeSpec.Core.Interface]
α:33 [in FreeSpec.Core.Hoare]
α:33 [in FreeSpec.Core.SemanticsFacts]
α:37 [in FreeSpec.Core.Contract]
α:39 [in FreeSpec.Core.Impure]
α:4 [in FreeSpec.Core.Semantics]
α:44 [in FreeSpec.Core.Contract]
α:5 [in FreeSpec.Core.Contract]
α:53 [in FreeSpec.Core.Contract]
α:57 [in FreeSpec.Core.SemanticsFacts]
α:6 [in FreeSpec.Core.Semantics]
α:6 [in FreeSpec.Core.Init]
α:61 [in FreeSpec.Core.Contract]
α:62 [in FreeSpec.Core.Semantics]
α:7 [in FreeSpec.Core.Hoare]
α:78 [in FreeSpec.Core.Contract]
α:79 [in FreeSpec.Core.SemanticsFacts]
α:8 [in FreeSpec.Core.Contract]
α:82 [in FreeSpec.Core.Contract]
α:85 [in FreeSpec.Core.Contract]
α:85 [in FreeSpec.Core.SemanticsFacts]
α:90 [in FreeSpec.Core.Contract]
α:91 [in FreeSpec.Core.SemanticsFacts]
α:95 [in FreeSpec.Core.Contract]
α:97 [in FreeSpec.Core.SemanticsFacts]
β:11 [in FreeSpec.Core.Impure]
β:14 [in FreeSpec.Core.Hoare]
β:19 [in FreeSpec.Core.Impure]
β:27 [in FreeSpec.Core.Hoare]
β:29 [in FreeSpec.Core.Impure]
β:31 [in FreeSpec.Core.ImpureFacts]
β:34 [in FreeSpec.Core.Hoare]
β:6 [in FreeSpec.Core.ImpureFacts]
β:6 [in FreeSpec.Core.Impure]
δ:32 [in FreeSpec.Core.ImpureFacts]
ωi:22 [in FreeSpec.Core.ComponentFacts]
ωi:42 [in FreeSpec.Core.ComponentFacts]
ωi:81 [in FreeSpec.Core.HoareFacts]
ωj':29 [in FreeSpec.Core.ComponentFacts]
ωj:23 [in FreeSpec.Core.ComponentFacts]
ωj:43 [in FreeSpec.Core.ComponentFacts]
ωj:83 [in FreeSpec.Core.HoareFacts]
ωmc:118 [in FreeSpec.Example.smram]
ωmem:119 [in FreeSpec.Example.smram]
ω'':67 [in FreeSpec.Core.HoareFacts]
ω':108 [in FreeSpec.Example.airlock]
ω':49 [in FreeSpec.Core.Hoare]
ω':49 [in FreeSpec.Core.HoareFacts]
ω':64 [in FreeSpec.Core.HoareFacts]
ω':93 [in FreeSpec.Example.airlock]
ω:10 [in FreeSpec.Core.Contract]
ω:100 [in FreeSpec.Example.smram]
ω:104 [in FreeSpec.Example.smram]
ω:105 [in FreeSpec.Example.airlock]
ω:119 [in FreeSpec.Example.airlock]
ω:137 [in FreeSpec.Example.smram]
ω:152 [in FreeSpec.Example.smram]
ω:17 [in FreeSpec.Core.Instrument]
ω:17 [in FreeSpec.Core.InstrumentFacts]
ω:20 [in FreeSpec.Core.Contract]
ω:23 [in FreeSpec.Core.SemanticsFacts]
ω:26 [in FreeSpec.Core.InstrumentFacts]
ω:27 [in FreeSpec.Core.Contract]
ω:33 [in FreeSpec.Core.HoareFacts]
ω:35 [in FreeSpec.Core.SemanticsFacts]
ω:36 [in FreeSpec.Core.Contract]
ω:36 [in FreeSpec.Core.InstrumentFacts]
ω:4 [in FreeSpec.Core.Contract]
ω:44 [in FreeSpec.Core.HoareFacts]
ω:46 [in FreeSpec.Core.Contract]
ω:47 [in FreeSpec.Core.Hoare]
ω:48 [in FreeSpec.Example.airlock]
ω:50 [in FreeSpec.Core.Hoare]
ω:51 [in FreeSpec.Example.airlock]
ω:53 [in FreeSpec.Example.airlock]
ω:54 [in FreeSpec.Example.airlock]
ω:55 [in FreeSpec.Core.Contract]
ω:62 [in FreeSpec.Core.HoareFacts]
ω:63 [in FreeSpec.Core.Contract]
ω:63 [in FreeSpec.Example.airlock]
ω:65 [in FreeSpec.Example.airlock]
ω:7 [in FreeSpec.Core.Contract]
ω:71 [in FreeSpec.Example.airlock]
ω:75 [in FreeSpec.Example.airlock]
ω:77 [in FreeSpec.Core.Contract]
ω:8 [in FreeSpec.Core.InstrumentFacts]
ω:80 [in FreeSpec.Example.airlock]
ω:81 [in FreeSpec.Core.Contract]
ω:82 [in FreeSpec.Example.smram]
ω:84 [in FreeSpec.Core.Contract]
ω:85 [in FreeSpec.Example.airlock]
ω:86 [in FreeSpec.Example.smram]
ω:9 [in FreeSpec.Core.Instrument]
ω:9 [in FreeSpec.Core.SemanticsFacts]
ω:90 [in FreeSpec.Example.smram]
ω:91 [in FreeSpec.Example.airlock]
ω:96 [in FreeSpec.Example.airlock]

Library Index

A

C

Component
ComponentFacts
Contract
Core
CoreFacts

E

Eval
Exec
Extraction

F

FFI

H

heap
Hoare
HoareFacts

I

Impure
ImpureFacts
Init
Instrument
InstrumentFacts
Interface

M

ML

R

Refs

S

Semantics
SemanticsFacts
smram

T

Lemma Index

B

bind_request_then_assoc [in FreeSpec.Core.ImpureFacts]

C

close_door_run [in FreeSpec.Example.airlock]
close_door_respectful [in FreeSpec.Example.airlock]
compliant_semantics_caller_obligation_compliant [in FreeSpec.Core.SemanticsFacts]
compliant_semantics_caller_obligation_callee_obligation [in FreeSpec.Core.SemanticsFacts]
controller_correct [in FreeSpec.Example.airlock]
correct_component_derives_compliant_semantics [in FreeSpec.Core.ComponentFacts]

D

derive_semantics_equ [in FreeSpec.Core.ComponentFacts]

E

eval_impure_bind_assoc [in FreeSpec.Core.SemanticsFacts]
eval_impure_request_then_assoc [in FreeSpec.Core.SemanticsFacts]
eval_semprod_in_right_eq [in FreeSpec.Core.SemanticsFacts]
eval_semprod_in_left_eq [in FreeSpec.Core.SemanticsFacts]
exec_impure_bind_assoc [in FreeSpec.Core.SemanticsFacts]
exec_impure_request_then_assoc [in FreeSpec.Core.SemanticsFacts]
exec_semprod_in_right_eq [in FreeSpec.Core.SemanticsFacts]
exec_semprod_in_left_eq [in FreeSpec.Core.SemanticsFacts]

I

impure_bind_assoc [in FreeSpec.Core.ImpureFacts]
impure_bind_local [in FreeSpec.Core.ImpureFacts]
instrument_preserves_compliance [in FreeSpec.Core.InstrumentFacts]
instrument_satisfies_hoare [in FreeSpec.Core.InstrumentFacts]
instrument_to_state_exec_morphism [in FreeSpec.Core.InstrumentFacts]
instrument_to_state_eval_morphism [in FreeSpec.Core.InstrumentFacts]

M

memory_controller_correct [in FreeSpec.Example.smram]
memory_controller_respectful [in FreeSpec.Example.smram]

N

no_contract_compliant_semantics [in FreeSpec.Core.SemanticsFacts]

O

one_door_safe_all_doors_safe [in FreeSpec.Example.airlock]
open_door_respectful [in FreeSpec.Example.airlock]

R

respectful_run_inv [in FreeSpec.Example.airlock]
run_effect_equation [in FreeSpec.Core.Semantics]
run_impure_bind_assoc [in FreeSpec.Core.SemanticsFacts]
run_impure_request_then_assoc [in FreeSpec.Core.SemanticsFacts]
run_impure_equation [in FreeSpec.Core.SemanticsFacts]

S

store_complies_to_store_specs [in FreeSpec.Core.SemanticsFacts]

T

tog_equ_2 [in FreeSpec.Example.airlock]
tog_equ_1 [in FreeSpec.Example.airlock]
to_hoare_contractprod [in FreeSpec.Core.HoareFacts]
to_hoare_post_bind_assoc [in FreeSpec.Core.HoareFacts]
to_hoare_pre_bind_assoc [in FreeSpec.Core.HoareFacts]
to_hoare_step [in FreeSpec.Core.HoareFacts]

Constructor Index

A

Assign [in FreeSpec.FFI.Refs]

C

compliant_semantics_rec [in FreeSpec.Core.SemanticsFacts]

D

Deref [in FreeSpec.FFI.Refs]
doors_o_callee_toggle [in FreeSpec.Example.airlock]
doors_o_callee_is_open [in FreeSpec.Example.airlock]

E

Eval [in FreeSpec.Exec.Eval]

G

Get [in FreeSpec.Core.Interface]
get_o_callee [in FreeSpec.Core.Contract]

I

in_right [in FreeSpec.Core.Interface]
in_left [in FreeSpec.Core.Interface]
IsOpen [in FreeSpec.Example.airlock]

L

left [in FreeSpec.Example.airlock]
local [in FreeSpec.Core.Impure]
local_eq [in FreeSpec.Core.ImpureFacts]

M

MakeDRAM [in FreeSpec.Example.smram]
MakeVGA [in FreeSpec.Example.smram]
make_contract [in FreeSpec.Core.Contract]
Make_ref [in FreeSpec.FFI.Refs]
memory_controller_write_o_callee [in FreeSpec.Example.smram]
memory_controller_read_o_callee [in FreeSpec.Example.smram]
mk_hoare [in FreeSpec.Core.Hoare]
mk_no_callee_obligation [in FreeSpec.Core.Contract]
mk_no_caller_obligation [in FreeSpec.Core.Contract]
mk_semantics [in FreeSpec.Core.Semantics]
mk_hoare_eq [in FreeSpec.Core.HoareFacts]

P

Put [in FreeSpec.Core.Interface]
put_o_callee [in FreeSpec.Core.Contract]

R

Read [in FreeSpec.Example.smram]
ReadFrom [in FreeSpec.Example.smram]
read_in_smram [in FreeSpec.Example.smram]
RequestOpen [in FreeSpec.Example.airlock]
request_eq [in FreeSpec.Core.ImpureFacts]
request_then [in FreeSpec.Core.Impure]
req_toggle [in FreeSpec.Example.airlock]
req_is_open [in FreeSpec.Example.airlock]
right [in FreeSpec.Example.airlock]

S

semantics_eq_rec [in FreeSpec.Core.SemanticsFacts]
smiact_unset [in FreeSpec.Example.smram]
smiact_set [in FreeSpec.Example.smram]

T

Tick [in FreeSpec.Example.airlock]
Toggle [in FreeSpec.Example.airlock]

W

write [in FreeSpec.Example.smram]
Write [in FreeSpec.Example.smram]
WriteTo [in FreeSpec.Example.smram]

Axiom Index

A

address [in FreeSpec.Example.smram]
address_eq_dec [in FreeSpec.Example.smram]
address_eq_refl [in FreeSpec.Example.smram]
address_eq [in FreeSpec.Example.smram]

C

cell [in FreeSpec.Example.smram]

I

in_smram_morphism [in FreeSpec.Example.smram]
in_smram [in FreeSpec.Example.smram]
io_assign [in FreeSpec.FFI.Refs]
io_deref [in FreeSpec.FFI.Refs]
io_make_ref [in FreeSpec.FFI.Refs]

R

reference [in FreeSpec.FFI.Refs]

Inductive Index

C

compliant_semantics [in FreeSpec.Core.SemanticsFacts]
CONTROLLER [in FreeSpec.Example.airlock]

D

door [in FreeSpec.Example.airlock]
DOORS [in FreeSpec.Example.airlock]
doors_o_callee [in FreeSpec.Example.airlock]
doors_o_caller [in FreeSpec.Example.airlock]
DRAM [in FreeSpec.Example.smram]
dram_o_callee [in FreeSpec.Example.smram]

E

EVAL [in FreeSpec.Exec.Eval]

H

hoare_eq [in FreeSpec.Core.HoareFacts]

I

iempty [in FreeSpec.Core.Interface]
impure [in FreeSpec.Core.Impure]
impure_eq [in FreeSpec.Core.ImpureFacts]
iplus [in FreeSpec.Core.Interface]

M

MEMORY [in FreeSpec.Example.smram]
memory_controller_o_callee [in FreeSpec.Example.smram]
MEMORY_CONTROLLER [in FreeSpec.Example.smram]

N

no_callee_obligation [in FreeSpec.Core.Contract]
no_caller_obligation [in FreeSpec.Core.Contract]

O

o_callee_store [in FreeSpec.Core.Contract]

R

REFS [in FreeSpec.FFI.Refs]

S

semantics [in FreeSpec.Core.Semantics]
semantics_eq [in FreeSpec.Core.SemanticsFacts]
smiact [in FreeSpec.Example.smram]
STORE [in FreeSpec.Core.Interface]

V

VGA [in FreeSpec.Example.smram]

Projection Index

A

assign [in FreeSpec.FFI.Refs]

C

callee_obligation [in FreeSpec.Core.Contract]
caller_obligation [in FreeSpec.Core.Contract]

D

deref [in FreeSpec.FFI.Refs]
distinguish [in FreeSpec.Core.Interface]

I

inj_p [in FreeSpec.Core.Interface]

M

make_ref [in FreeSpec.FFI.Refs]

P

post [in FreeSpec.Core.Hoare]
pre [in FreeSpec.Core.Hoare]
proj_inj_p_equ [in FreeSpec.Core.Interface]
proj_p [in FreeSpec.Core.Interface]

W

witness_update [in FreeSpec.Core.Contract]

Instance Index

C

compliant_semantics_Proper [in FreeSpec.Core.SemanticsFacts]

D

default_MayProvide [in FreeSpec.Core.Interface]

E

eval_impure_Proper [in FreeSpec.Core.SemanticsFacts]
eval_effect_Proper [in FreeSpec.Core.SemanticsFacts]
exec_impure_Proper [in FreeSpec.Core.SemanticsFacts]
exec_effect_Proper [in FreeSpec.Core.SemanticsFacts]

F

FreeSpec_Inject [in FreeSpec.FFI.FFI]
fst_Proper [in FreeSpec.Core.SemanticsFacts]
function_eq_Equivalence [in FreeSpec.Core.Init]

H

hoare_Monad [in FreeSpec.Core.Hoare]
hoare_Applicative [in FreeSpec.Core.Hoare]
hoare_Functor [in FreeSpec.Core.Hoare]
hoare_Equivalence [in FreeSpec.Core.HoareFacts]

I

impure_apply_Proper [in FreeSpec.Core.ImpureFacts]
impure_map_Proper [in FreeSpec.Core.ImpureFacts]
impure_bind_Proper [in FreeSpec.Core.ImpureFacts]
impure_Equivalence [in FreeSpec.Core.ImpureFacts]
impure_Monad [in FreeSpec.Core.Impure]
impure_Applicative [in FreeSpec.Core.Impure]
impure_Functor [in FreeSpec.Core.Impure]
iplus_right_distinguish_right_Distinguish [in FreeSpec.Core.Interface]
iplus_left_distinguish_left_Distinguish [in FreeSpec.Core.Interface]
iplus_right_may_left_Distinguish [in FreeSpec.Core.Interface]
iplus_left_may_right_Distinguish [in FreeSpec.Core.Interface]
iplus_right_default_Distinguish [in FreeSpec.Core.Interface]
iplus_left_default_Distinguish [in FreeSpec.Core.Interface]
iplus_right_Provide [in FreeSpec.Core.Interface]
iplus_right_MayProvide [in FreeSpec.Core.Interface]
iplus_left_Provide [in FreeSpec.Core.Interface]
iplus_left_MayProvide [in FreeSpec.Core.Interface]

M

Make_StrictProvide5 [in FreeSpec.Core.Interface]
Make_StrictProvide4 [in FreeSpec.Core.Interface]
Make_StrictProvide3 [in FreeSpec.Core.Interface]
Make_StrictProvide2 [in FreeSpec.Core.Interface]
Make_Provide5 [in FreeSpec.Core.Interface]
Make_Provide4 [in FreeSpec.Core.Interface]
Make_Provide3 [in FreeSpec.Core.Interface]
Make_Provide2 [in FreeSpec.Core.Interface]
MonadRefs_Inject [in FreeSpec.FFI.Refs]
MonadRefs_IO [in FreeSpec.FFI.Refs]

P

post_Proper [in FreeSpec.Core.HoareFacts]
pre_Proper [in FreeSpec.Core.HoareFacts]
prod_Proper [in FreeSpec.Core.SemanticsFacts]

R

refl_Distinguish [in FreeSpec.Core.Interface]
refl_Provide [in FreeSpec.Core.Interface]
refl_MayProvide [in FreeSpec.Core.Interface]
request_then_Proper [in FreeSpec.Core.ImpureFacts]
run_impure_Proper_2 [in FreeSpec.Core.SemanticsFacts]
run_impure_Proper_1 [in FreeSpec.Core.SemanticsFacts]
run_effect_Proper [in FreeSpec.Core.SemanticsFacts]
run_effect_Equivalence [in FreeSpec.Core.SemanticsFacts]

S

semantics_Equivalence [in FreeSpec.Core.SemanticsFacts]
semprod_Proper [in FreeSpec.Core.SemanticsFacts]
snd_Proper [in FreeSpec.Core.SemanticsFacts]
store_monad_state [in FreeSpec.Core.Impure]

T

to_hoare_Proper [in FreeSpec.Core.HoareFacts]

Abbreviation Index

I

instrument [in FreeSpec.Core.Instrument]
interp [in FreeSpec.Core.Semantics]

Definition Index

B

bootstrap [in FreeSpec.Core.Component]

C

close_door [in FreeSpec.Example.airlock]
co [in FreeSpec.Example.airlock]
component [in FreeSpec.Core.Component]
const_witness [in FreeSpec.Core.Contract]
contractprod [in FreeSpec.Core.Contract]
controller [in FreeSpec.Example.airlock]
correct_component [in FreeSpec.Core.ComponentFacts]

D

derive_semantics' [in FreeSpec.Core.ComponentFacts]
derive_semantics [in FreeSpec.Core.Component]
dispatch [in FreeSpec.Example.smram]
doors_contract [in FreeSpec.Example.airlock]
door_eq_dec [in FreeSpec.Example.airlock]
do_no_use [in FreeSpec.Core.Contract]
dram_specs [in FreeSpec.Example.smram]
dram_write_to [in FreeSpec.Example.smram]
dram_read_from [in FreeSpec.Example.smram]

E

eval [in FreeSpec.Exec.Eval]
eval_impure [in FreeSpec.Core.Semantics]
eval_effect [in FreeSpec.Core.Semantics]
exec_impure [in FreeSpec.Core.Semantics]
exec_effect [in FreeSpec.Core.Semantics]

F

forbid_specs [in FreeSpec.Core.Contract]
function_eq [in FreeSpec.Core.Init]

G

gen_callee_obligation [in FreeSpec.Core.Contract]
gen_caller_obligation [in FreeSpec.Core.Contract]
gen_witness_update [in FreeSpec.Core.Contract]

H

hoare_apply [in FreeSpec.Core.Hoare]
hoare_map [in FreeSpec.Core.Hoare]
hoare_bind [in FreeSpec.Core.Hoare]
hoare_pure [in FreeSpec.Core.Hoare]

I

iempty_semantics [in FreeSpec.Core.Semantics]
impure_lift [in FreeSpec.Core.Impure]
impure_apply [in FreeSpec.Core.Impure]
impure_pure [in FreeSpec.Core.Impure]
impure_map [in FreeSpec.Core.Impure]
impure_bind [in FreeSpec.Core.Impure]
inj_assign [in FreeSpec.FFI.Refs]
inj_deref [in FreeSpec.FFI.Refs]
inj_make_ref [in FreeSpec.FFI.Refs]
instrument_to_state [in FreeSpec.Core.Instrument]
interface [in FreeSpec.Core.Interface]
interface_to_hoare [in FreeSpec.Core.Hoare]
interface_to_state [in FreeSpec.Core.Semantics]
interface_to_instrument [in FreeSpec.Core.Instrument]
is_open [in FreeSpec.Example.airlock]

M

mc_specs [in FreeSpec.Example.smram]
memory_view [in FreeSpec.Example.smram]
memory_controller [in FreeSpec.Example.smram]

N

no_contract [in FreeSpec.Core.Contract]

O

open_door [in FreeSpec.Example.airlock]

R

request [in FreeSpec.Core.Impure]
request_open [in FreeSpec.Example.airlock]
run_impure [in FreeSpec.Core.Semantics]
run_effect [in FreeSpec.Core.Semantics]
run_effect_eq [in FreeSpec.Core.SemanticsFacts]

S

sel [in FreeSpec.Example.airlock]
semprod [in FreeSpec.Core.Semantics]
smram_pred [in FreeSpec.Example.smram]
step [in FreeSpec.Example.airlock]
store [in FreeSpec.Core.Semantics]
store_specs [in FreeSpec.Core.Contract]
store_update [in FreeSpec.Core.Contract]

T

tick [in FreeSpec.Example.airlock]
tog [in FreeSpec.Example.airlock]
toggle [in FreeSpec.Example.airlock]
to_hoare [in FreeSpec.Core.Hoare]
to_state [in FreeSpec.Core.Semantics]
to_instrument [in FreeSpec.Core.Instrument]

U

unwrap_sumbool [in FreeSpec.Example.smram]
update_memory_controller_view [in FreeSpec.Example.smram]
update_dram_view [in FreeSpec.Example.smram]
update_memory_view_address [in FreeSpec.Example.smram]

V

vga_write_to [in FreeSpec.Example.smram]
vga_read_from [in FreeSpec.Example.smram]

W

when [in FreeSpec.Core.Init]
with_store [in FreeSpec.Core.Semantics]
with_semantics [in FreeSpec.Core.Semantics]
with_component [in FreeSpec.Core.Component]
with_component_aux [in FreeSpec.Core.Component]
with_heap_impure [in FreeSpec.Example.heap]
with_heap [in FreeSpec.Example.heap]

other

Ω [in FreeSpec.Example.airlock]

Record Index

C

contract [in FreeSpec.Core.Contract]

D

Distinguish [in FreeSpec.Core.Interface]

H

hoare [in FreeSpec.Core.Hoare]

M

MayProvide [in FreeSpec.Core.Interface]
MonadRefs [in FreeSpec.FFI.Refs]

P

Provide [in FreeSpec.Core.Interface]
Provide2 [in FreeSpec.Core.Interface]
Provide3 [in FreeSpec.Core.Interface]
Provide4 [in FreeSpec.Core.Interface]
Provide5 [in FreeSpec.Core.Interface]

S

StrictProvide2 [in FreeSpec.Core.Interface]
StrictProvide3 [in FreeSpec.Core.Interface]
StrictProvide4 [in FreeSpec.Core.Interface]
StrictProvide5 [in FreeSpec.Core.Interface]

Global Index

Z

_

(1466 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

_

(6 entries)

Binder Index

T

W

Z

_

(1148 entries)

Library Index

B

D

G

J

K

L

N

O

P

Q

U

V

W

X

Y

Z

_

other

(25 entries)

Lemma Index

A

F

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(39 entries)

Constructor Index

B

F

H

J

K

N

O

Q

U

V

X

Y

Z

_

other

(44 entries)

Axiom Index

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

Inductive Index

A

B

F

G

J

K

L

P

Q

T

U

W

X

Y

Z

_

other

(26 entries)

Projection Index

B

E

F

G

H

J

K

L

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(12 entries)

Instance Index

A

B

G

J

K

L

N

O

Q

U

V

W

X

Y

Z

_

other

(56 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

J

K

L

P

Q

X

Y

Z

_

(83 entries)

Record Index

A

B

E

F

G

I

J

K

L

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

This page has been generated by coqdoc