| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2056 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (66 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1535 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (152 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (163 entries) |
Global Index
A
A [definition, in SpecCT]ACTIf [constructor, in SpecCT]
add42_monotonic [lemma, in RelHoare]
add42_monotonic_spec [definition, in RelHoare]
aeval [definition, in SpecCT]
aeval_unused_update [lemma, in SpecCT]
aeval_beval_unused_update [lemma, in SpecCT]
aexp [inductive, in SpecCT]
Aexp [definition, in RelHoare]
aexp_bexp_has_label_mutind [definition, in SpecCT]
aexp_bexp_has_label_ind [definition, in SpecCT]
aexp_has_label [inductive, in SpecCT]
aexp_bexp_mutind [definition, in SpecCT]
aexp_bexp_ind [definition, in SpecCT]
Aexp_of_aexp_2 [definition, in RelHoare]
Aexp_of_aexp_1 [definition, in RelHoare]
Aexp_of_nat [definition, in RelHoare]
aexp_has_label [inductive, in StaticIFC]
ae:741 [binder, in SpecCT]
ae:745 [binder, in SpecCT]
AId [constructor, in SpecCT]
AMinus [constructor, in SpecCT]
AMult [constructor, in SpecCT]
ANum [constructor, in SpecCT]
AP [definition, in SpecCT]
ap [definition, in RelHoare]
APlus [constructor, in SpecCT]
app_eq_prefix [lemma, in SpecCT]
ap2 [definition, in RelHoare]
ARead [constructor, in SpecCT]
arr_a':882 [binder, in SpecCT]
arr_a:877 [binder, in SpecCT]
arr_a':875 [binder, in SpecCT]
arr_a:871 [binder, in SpecCT]
AS [definition, in SpecCT]
Asgn [constructor, in SpecCT]
assn_sub_2 [definition, in RelHoare]
assn_sub_1 [definition, in RelHoare]
astate [definition, in SpecCT]
astt1:922 [binder, in SpecCT]
astt1:930 [binder, in SpecCT]
astt2:926 [binder, in SpecCT]
astt2:934 [binder, in SpecCT]
ast'':283 [binder, in SpecCT]
ast'':452 [binder, in SpecCT]
ast'':81 [binder, in SpecCT]
ast':104 [binder, in SpecCT]
ast':280 [binder, in SpecCT]
ast':293 [binder, in SpecCT]
ast':304 [binder, in SpecCT]
ast':317 [binder, in SpecCT]
ast':404 [binder, in SpecCT]
ast':412 [binder, in SpecCT]
ast':449 [binder, in SpecCT]
ast':462 [binder, in SpecCT]
ast':473 [binder, in SpecCT]
ast':486 [binder, in SpecCT]
ast':733 [binder, in SpecCT]
ast':758 [binder, in SpecCT]
ast':770 [binder, in SpecCT]
ast':782 [binder, in SpecCT]
ast':79 [binder, in SpecCT]
ast':794 [binder, in SpecCT]
ast':87 [binder, in SpecCT]
ast':903 [binder, in SpecCT]
ast':916 [binder, in SpecCT]
ast':95 [binder, in SpecCT]
ast1':146 [binder, in SpecCT]
ast1':362 [binder, in SpecCT]
ast1':423 [binder, in SpecCT]
ast1':635 [binder, in SpecCT]
ast1':808 [binder, in SpecCT]
ast1:142 [binder, in SpecCT]
ast1:358 [binder, in SpecCT]
ast1:419 [binder, in SpecCT]
ast1:630 [binder, in SpecCT]
ast1:672 [binder, in SpecCT]
ast1:804 [binder, in SpecCT]
ast2':147 [binder, in SpecCT]
ast2':363 [binder, in SpecCT]
ast2':424 [binder, in SpecCT]
ast2':636 [binder, in SpecCT]
ast2':809 [binder, in SpecCT]
ast2:143 [binder, in SpecCT]
ast2:359 [binder, in SpecCT]
ast2:420 [binder, in SpecCT]
ast2:631 [binder, in SpecCT]
ast2:673 [binder, in SpecCT]
ast2:805 [binder, in SpecCT]
ast:102 [binder, in SpecCT]
ast:108 [binder, in SpecCT]
ast:114 [binder, in SpecCT]
ast:266 [binder, in SpecCT]
ast:269 [binder, in SpecCT]
ast:277 [binder, in SpecCT]
ast:290 [binder, in SpecCT]
ast:301 [binder, in SpecCT]
ast:313 [binder, in SpecCT]
ast:322 [binder, in SpecCT]
ast:329 [binder, in SpecCT]
ast:337 [binder, in SpecCT]
ast:345 [binder, in SpecCT]
ast:402 [binder, in SpecCT]
ast:410 [binder, in SpecCT]
ast:435 [binder, in SpecCT]
ast:438 [binder, in SpecCT]
ast:446 [binder, in SpecCT]
ast:459 [binder, in SpecCT]
ast:470 [binder, in SpecCT]
ast:482 [binder, in SpecCT]
ast:491 [binder, in SpecCT]
ast:498 [binder, in SpecCT]
ast:506 [binder, in SpecCT]
ast:514 [binder, in SpecCT]
ast:68 [binder, in SpecCT]
ast:70 [binder, in SpecCT]
ast:730 [binder, in SpecCT]
ast:753 [binder, in SpecCT]
ast:765 [binder, in SpecCT]
ast:77 [binder, in SpecCT]
ast:777 [binder, in SpecCT]
ast:791 [binder, in SpecCT]
ast:85 [binder, in SpecCT]
ast:888 [binder, in SpecCT]
ast:898 [binder, in SpecCT]
ast:912 [binder, in SpecCT]
ast:93 [binder, in SpecCT]
aux [lemma, in SpecCT]
AWrite [constructor, in SpecCT]
ax:398 [binder, in SpecCT]
a_unused [definition, in SpecCT]
a':334 [binder, in SpecCT]
a':351 [binder, in SpecCT]
a':377 [binder, in SpecCT]
a':386 [binder, in SpecCT]
a':395 [binder, in SpecCT]
a':503 [binder, in SpecCT]
a':520 [binder, in SpecCT]
a':529 [binder, in SpecCT]
a':540 [binder, in SpecCT]
a':550 [binder, in SpecCT]
a':559 [binder, in SpecCT]
a':568 [binder, in SpecCT]
a1':250 [binder, in SpecCT]
a1':653 [binder, in SpecCT]
a1':690 [binder, in SpecCT]
a1:11 [binder, in SpecCT]
a1:14 [binder, in SpecCT]
a1:16 [binder, in SpecCT]
a1:165 [binder, in SpecCT]
a1:169 [binder, in SpecCT]
a1:173 [binder, in SpecCT]
a1:179 [binder, in SpecCT]
a1:18 [binder, in SpecCT]
a1:183 [binder, in SpecCT]
a1:187 [binder, in SpecCT]
a1:191 [binder, in SpecCT]
a1:195 [binder, in SpecCT]
a1:20 [binder, in SpecCT]
a1:22 [binder, in SpecCT]
a1:246 [binder, in SpecCT]
a1:38 [binder, in StaticIFC]
a1:42 [binder, in StaticIFC]
a1:46 [binder, in StaticIFC]
a1:616 [binder, in SpecCT]
a1:623 [binder, in SpecCT]
a1:648 [binder, in SpecCT]
a1:66 [binder, in StaticIFC]
a1:664 [binder, in SpecCT]
a1:685 [binder, in SpecCT]
a1:7 [binder, in SpecCT]
a1:70 [binder, in StaticIFC]
a1:74 [binder, in StaticIFC]
a1:78 [binder, in StaticIFC]
a1:9 [binder, in SpecCT]
a1:92 [binder, in RelHoare]
a2':251 [binder, in SpecCT]
a2':654 [binder, in SpecCT]
a2':691 [binder, in SpecCT]
a2:10 [binder, in SpecCT]
a2:12 [binder, in SpecCT]
a2:15 [binder, in SpecCT]
a2:167 [binder, in SpecCT]
a2:17 [binder, in SpecCT]
a2:171 [binder, in SpecCT]
a2:175 [binder, in SpecCT]
a2:181 [binder, in SpecCT]
a2:185 [binder, in SpecCT]
a2:189 [binder, in SpecCT]
a2:19 [binder, in SpecCT]
a2:193 [binder, in SpecCT]
a2:197 [binder, in SpecCT]
a2:21 [binder, in SpecCT]
a2:23 [binder, in SpecCT]
a2:247 [binder, in SpecCT]
a2:40 [binder, in StaticIFC]
a2:44 [binder, in StaticIFC]
a2:48 [binder, in StaticIFC]
a2:617 [binder, in SpecCT]
a2:624 [binder, in SpecCT]
a2:649 [binder, in SpecCT]
a2:665 [binder, in SpecCT]
a2:68 [binder, in StaticIFC]
a2:686 [binder, in SpecCT]
a2:72 [binder, in StaticIFC]
a2:76 [binder, in StaticIFC]
a2:8 [binder, in SpecCT]
a2:80 [binder, in StaticIFC]
a2:93 [binder, in RelHoare]
a:110 [binder, in SpecCT]
a:115 [binder, in SpecCT]
a:127 [binder, in StaticIFC]
a:152 [binder, in StaticIFC]
a:206 [binder, in StaticIFC]
a:208 [binder, in SpecCT]
a:215 [binder, in SpecCT]
a:225 [binder, in SpecCT]
a:235 [binder, in SpecCT]
a:237 [binder, in SpecCT]
a:239 [binder, in StaticIFC]
a:259 [binder, in SpecCT]
a:261 [binder, in SpecCT]
a:325 [binder, in SpecCT]
a:331 [binder, in SpecCT]
a:339 [binder, in SpecCT]
a:346 [binder, in SpecCT]
a:373 [binder, in SpecCT]
a:382 [binder, in SpecCT]
a:39 [binder, in SpecCT]
a:391 [binder, in SpecCT]
a:41 [binder, in SpecCT]
a:45 [binder, in SpecCT]
a:494 [binder, in SpecCT]
a:500 [binder, in SpecCT]
a:508 [binder, in SpecCT]
a:51 [binder, in StaticIFC]
a:515 [binder, in SpecCT]
a:525 [binder, in SpecCT]
a:536 [binder, in SpecCT]
a:546 [binder, in SpecCT]
a:55 [binder, in StaticIFC]
a:557 [binder, in SpecCT]
a:566 [binder, in SpecCT]
a:57 [binder, in StaticIFC]
a:61 [binder, in SpecCT]
A:612 [binder, in SpecCT]
A:619 [binder, in SpecCT]
a:62 [binder, in StaticIFC]
a:63 [binder, in SpecCT]
a:698 [binder, in SpecCT]
a:7 [binder, in RelHoare]
a:80 [binder, in RelHoare]
A:815 [binder, in SpecCT]
A:818 [binder, in SpecCT]
A:819 [binder, in SpecCT]
A:822 [binder, in SpecCT]
a:847 [binder, in SpecCT]
a:85 [binder, in RelHoare]
a:89 [binder, in StaticIFC]
a:9 [binder, in RelHoare]
a:96 [binder, in RelHoare]
a:99 [binder, in RelHoare]
B
BAnd [constructor, in SpecCT]bassn_2 [definition, in RelHoare]
bassn_1 [definition, in RelHoare]
BEq [constructor, in SpecCT]
beval [definition, in SpecCT]
beval_unused_update [lemma, in SpecCT]
bexp [inductive, in SpecCT]
bexp_aexp_has_label_ind [definition, in SpecCT]
bexp_has_label [inductive, in SpecCT]
bexp_aexp_ind [definition, in SpecCT]
bexp_eval_false_2 [lemma, in RelHoare]
bexp_eval_false_1 [lemma, in RelHoare]
bexp_has_label [inductive, in StaticIFC]
be:177 [binder, in SpecCT]
be:295 [binder, in SpecCT]
be:306 [binder, in SpecCT]
be:311 [binder, in SpecCT]
be:33 [binder, in SpecCT]
be:36 [binder, in SpecCT]
be:464 [binder, in SpecCT]
be:475 [binder, in SpecCT]
be:480 [binder, in SpecCT]
be:742 [binder, in SpecCT]
be:749 [binder, in SpecCT]
be:851 [binder, in SpecCT]
BFalse [constructor, in SpecCT]
BGt [constructor, in SpecCT]
BLe [constructor, in SpecCT]
BNeq [constructor, in SpecCT]
BNot [constructor, in SpecCT]
bool_value:867 [binder, in SpecCT]
branches [definition, in StaticIFC]
broken_def_accepts_insecure_f [lemma, in Noninterference]
broken_def_rejects_secure_f [lemma, in Noninterference]
broken_def [definition, in Noninterference]
bs1:247 [binder, in StaticIFC]
bs1:254 [binder, in StaticIFC]
bs1:260 [binder, in StaticIFC]
bs1:275 [binder, in StaticIFC]
bs2:248 [binder, in StaticIFC]
bs2:276 [binder, in StaticIFC]
bs:268 [binder, in StaticIFC]
BTrue [constructor, in SpecCT]
bt1:923 [binder, in SpecCT]
bt1:931 [binder, in SpecCT]
bt2:927 [binder, in SpecCT]
bt2:935 [binder, in SpecCT]
b_unused [definition, in SpecCT]
b'':284 [binder, in SpecCT]
b'':453 [binder, in SpecCT]
b':281 [binder, in SpecCT]
b':294 [binder, in SpecCT]
b':305 [binder, in SpecCT]
b':318 [binder, in SpecCT]
b':378 [binder, in SpecCT]
b':387 [binder, in SpecCT]
b':396 [binder, in SpecCT]
b':450 [binder, in SpecCT]
b':463 [binder, in SpecCT]
b':474 [binder, in SpecCT]
b':487 [binder, in SpecCT]
b':530 [binder, in SpecCT]
b':541 [binder, in SpecCT]
b':551 [binder, in SpecCT]
b':734 [binder, in SpecCT]
b':759 [binder, in SpecCT]
b':771 [binder, in SpecCT]
b':783 [binder, in SpecCT]
b':795 [binder, in SpecCT]
b':904 [binder, in SpecCT]
b':917 [binder, in SpecCT]
b1':364 [binder, in SpecCT]
b1':637 [binder, in SpecCT]
b1':655 [binder, in SpecCT]
b1':692 [binder, in SpecCT]
b1':810 [binder, in SpecCT]
b1:161 [binder, in RelHoare]
b1:173 [binder, in RelHoare]
b1:185 [binder, in RelHoare]
b1:191 [binder, in RelHoare]
b1:201 [binder, in SpecCT]
b1:208 [binder, in RelHoare]
b1:213 [binder, in RelHoare]
b1:25 [binder, in SpecCT]
b1:674 [binder, in SpecCT]
b1:84 [binder, in StaticIFC]
b2':365 [binder, in SpecCT]
b2':638 [binder, in SpecCT]
b2':656 [binder, in SpecCT]
b2':693 [binder, in SpecCT]
b2':811 [binder, in SpecCT]
b2:162 [binder, in RelHoare]
b2:180 [binder, in RelHoare]
b2:198 [binder, in RelHoare]
b2:203 [binder, in SpecCT]
b2:204 [binder, in RelHoare]
b2:209 [binder, in RelHoare]
b2:216 [binder, in RelHoare]
b2:26 [binder, in SpecCT]
b2:675 [binder, in SpecCT]
b2:86 [binder, in StaticIFC]
b:100 [binder, in SpecCT]
b:100 [binder, in StaticIFC]
b:13 [binder, in SpecCT]
b:131 [binder, in StaticIFC]
b:134 [binder, in StaticIFC]
b:143 [binder, in RelHoare]
b:146 [binder, in RelHoare]
b:153 [binder, in RelHoare]
b:156 [binder, in RelHoare]
b:158 [binder, in StaticIFC]
b:163 [binder, in StaticIFC]
b:199 [binder, in SpecCT]
b:210 [binder, in SpecCT]
b:212 [binder, in StaticIFC]
b:216 [binder, in StaticIFC]
b:219 [binder, in SpecCT]
b:229 [binder, in SpecCT]
b:232 [binder, in SpecCT]
b:24 [binder, in SpecCT]
b:251 [binder, in StaticIFC]
b:257 [binder, in StaticIFC]
b:261 [binder, in StaticIFC]
b:267 [binder, in SpecCT]
b:270 [binder, in SpecCT]
b:278 [binder, in SpecCT]
b:291 [binder, in SpecCT]
b:302 [binder, in SpecCT]
b:314 [binder, in SpecCT]
b:323 [binder, in SpecCT]
b:338 [binder, in SpecCT]
b:374 [binder, in SpecCT]
b:383 [binder, in SpecCT]
b:392 [binder, in SpecCT]
b:436 [binder, in SpecCT]
b:439 [binder, in SpecCT]
b:447 [binder, in SpecCT]
b:460 [binder, in SpecCT]
b:47 [binder, in SpecCT]
b:471 [binder, in SpecCT]
b:483 [binder, in SpecCT]
b:492 [binder, in SpecCT]
b:507 [binder, in SpecCT]
b:526 [binder, in SpecCT]
b:537 [binder, in SpecCT]
b:547 [binder, in SpecCT]
b:60 [binder, in SpecCT]
b:632 [binder, in SpecCT]
b:650 [binder, in SpecCT]
b:666 [binder, in SpecCT]
b:687 [binder, in SpecCT]
b:700 [binder, in SpecCT]
b:731 [binder, in SpecCT]
b:754 [binder, in SpecCT]
b:766 [binder, in SpecCT]
b:778 [binder, in SpecCT]
b:792 [binder, in SpecCT]
b:82 [binder, in StaticIFC]
B:823 [binder, in SpecCT]
b:85 [binder, in Noninterference]
b:872 [binder, in SpecCT]
b:879 [binder, in SpecCT]
b:88 [binder, in SpecCT]
b:889 [binder, in SpecCT]
b:899 [binder, in SpecCT]
b:913 [binder, in SpecCT]
b:93 [binder, in StaticIFC]
b:95 [binder, in StaticIFC]
b:96 [binder, in SpecCT]
C
cannot_flow_secret_public [lemma, in StaticIFC]can_flow [definition, in SpecCT]
can_flow_join_r2 [lemma, in StaticIFC]
can_flow_join_r1 [lemma, in StaticIFC]
can_flow_join_l [lemma, in StaticIFC]
can_flow_join_2 [lemma, in StaticIFC]
can_flow_join_1 [lemma, in StaticIFC]
can_flow_trans [lemma, in StaticIFC]
can_flow_refl [lemma, in StaticIFC]
can_flow_secret [lemma, in StaticIFC]
can_flow_public [lemma, in StaticIFC]
can_flow [definition, in StaticIFC]
com [inductive, in SpecCT]
com_size [definition, in SpecCT]
constant_sme_insecure_f [lemma, in Noninterference]
cteval [inductive, in SpecCT]
cteval_equiv_seq_spec_eval [lemma, in SpecCT]
CTE_Write [constructor, in SpecCT]
CTE_ARead [constructor, in SpecCT]
CTE_While [constructor, in SpecCT]
CTE_IfFalse [constructor, in SpecCT]
CTE_IfTrue [constructor, in SpecCT]
CTE_Seq [constructor, in SpecCT]
CTE_Asgn [constructor, in SpecCT]
CTE_Skip [constructor, in SpecCT]
ct_well_typed_ideal_noninterferent [lemma, in SpecCT]
ct_well_typed_ideal_noninterferent_general [lemma, in SpecCT]
ct_well_typed_seq_spec_eval_ct_secure [lemma, in SpecCT]
ct_well_typed_ct_secure [lemma, in SpecCT]
ct_well_typed_noninterferent [lemma, in SpecCT]
CT_AWrite [constructor, in SpecCT]
CT_ARead [constructor, in SpecCT]
CT_While [constructor, in SpecCT]
CT_If [constructor, in SpecCT]
CT_Seq [constructor, in SpecCT]
CT_Asgn [constructor, in SpecCT]
CT_Skip [constructor, in SpecCT]
ct_well_typed [inductive, in SpecCT]
ct_insecure_prog_is_not_ct_secure [definition, in SpecCT]
ct_insecure_prog [definition, in SpecCT]
ct_secure [definition, in SpecCT]
c':717 [binder, in SpecCT]
c1:107 [binder, in RelHoare]
c1:113 [binder, in RelHoare]
c1:117 [binder, in RelHoare]
c1:121 [binder, in RelHoare]
c1:125 [binder, in RelHoare]
c1:129 [binder, in StaticIFC]
c1:130 [binder, in RelHoare]
c1:132 [binder, in StaticIFC]
c1:135 [binder, in StaticIFC]
c1:141 [binder, in RelHoare]
c1:155 [binder, in StaticIFC]
c1:160 [binder, in StaticIFC]
c1:165 [binder, in StaticIFC]
c1:179 [binder, in RelHoare]
c1:186 [binder, in StaticIFC]
c1:197 [binder, in RelHoare]
c1:203 [binder, in RelHoare]
c1:209 [binder, in StaticIFC]
c1:210 [binder, in RelHoare]
c1:214 [binder, in RelHoare]
c1:214 [binder, in StaticIFC]
c1:217 [binder, in StaticIFC]
c1:227 [binder, in SpecCT]
c1:230 [binder, in SpecCT]
c1:233 [binder, in SpecCT]
c1:242 [binder, in StaticIFC]
c1:252 [binder, in StaticIFC]
c1:258 [binder, in StaticIFC]
c1:274 [binder, in SpecCT]
c1:296 [binder, in SpecCT]
c1:307 [binder, in SpecCT]
c1:31 [binder, in SpecCT]
c1:34 [binder, in SpecCT]
c1:443 [binder, in SpecCT]
c1:465 [binder, in SpecCT]
c1:476 [binder, in SpecCT]
c1:55 [binder, in RelHoare]
c1:66 [binder, in RelHoare]
c1:71 [binder, in RelHoare]
c1:722 [binder, in SpecCT]
c1:74 [binder, in SpecCT]
c1:77 [binder, in RelHoare]
c1:89 [binder, in SpecCT]
c1:97 [binder, in SpecCT]
c2:108 [binder, in RelHoare]
c2:114 [binder, in RelHoare]
c2:118 [binder, in RelHoare]
c2:122 [binder, in RelHoare]
c2:126 [binder, in RelHoare]
c2:130 [binder, in StaticIFC]
c2:133 [binder, in StaticIFC]
c2:136 [binder, in RelHoare]
c2:142 [binder, in RelHoare]
c2:156 [binder, in StaticIFC]
c2:161 [binder, in StaticIFC]
c2:176 [binder, in RelHoare]
c2:187 [binder, in StaticIFC]
c2:188 [binder, in RelHoare]
c2:194 [binder, in RelHoare]
c2:210 [binder, in StaticIFC]
c2:211 [binder, in RelHoare]
c2:215 [binder, in StaticIFC]
c2:217 [binder, in RelHoare]
c2:228 [binder, in SpecCT]
c2:231 [binder, in SpecCT]
c2:243 [binder, in StaticIFC]
c2:253 [binder, in StaticIFC]
c2:259 [binder, in StaticIFC]
c2:275 [binder, in SpecCT]
c2:297 [binder, in SpecCT]
c2:308 [binder, in SpecCT]
c2:32 [binder, in SpecCT]
c2:35 [binder, in SpecCT]
c2:444 [binder, in SpecCT]
c2:466 [binder, in SpecCT]
c2:477 [binder, in SpecCT]
c2:56 [binder, in RelHoare]
c2:67 [binder, in RelHoare]
c2:72 [binder, in RelHoare]
c2:724 [binder, in SpecCT]
c2:75 [binder, in SpecCT]
c2:78 [binder, in RelHoare]
c2:90 [binder, in SpecCT]
c2:98 [binder, in SpecCT]
c:106 [binder, in SpecCT]
c:120 [binder, in Noninterference]
c:127 [binder, in Noninterference]
c:130 [binder, in Noninterference]
c:136 [binder, in Noninterference]
c:137 [binder, in StaticIFC]
c:139 [binder, in SpecCT]
c:141 [binder, in StaticIFC]
c:143 [binder, in Noninterference]
c:143 [binder, in StaticIFC]
c:145 [binder, in StaticIFC]
c:148 [binder, in Noninterference]
c:153 [binder, in Noninterference]
c:163 [binder, in Noninterference]
c:168 [binder, in Noninterference]
c:168 [binder, in StaticIFC]
c:173 [binder, in StaticIFC]
c:176 [binder, in Noninterference]
c:176 [binder, in StaticIFC]
c:178 [binder, in Noninterference]
c:180 [binder, in StaticIFC]
c:182 [binder, in Noninterference]
c:182 [binder, in StaticIFC]
c:19 [binder, in StaticIFC]
c:193 [binder, in StaticIFC]
c:195 [binder, in StaticIFC]
c:219 [binder, in StaticIFC]
c:222 [binder, in StaticIFC]
c:224 [binder, in StaticIFC]
c:228 [binder, in StaticIFC]
c:234 [binder, in StaticIFC]
c:243 [binder, in SpecCT]
c:256 [binder, in SpecCT]
c:264 [binder, in StaticIFC]
c:265 [binder, in StaticIFC]
c:270 [binder, in StaticIFC]
c:278 [binder, in StaticIFC]
c:320 [binder, in SpecCT]
c:355 [binder, in SpecCT]
c:37 [binder, in SpecCT]
c:371 [binder, in SpecCT]
c:380 [binder, in SpecCT]
c:389 [binder, in SpecCT]
c:400 [binder, in SpecCT]
c:408 [binder, in SpecCT]
c:416 [binder, in SpecCT]
c:428 [binder, in SpecCT]
c:489 [binder, in SpecCT]
c:523 [binder, in SpecCT]
c:534 [binder, in SpecCT]
c:544 [binder, in SpecCT]
c:555 [binder, in SpecCT]
c:564 [binder, in SpecCT]
c:627 [binder, in SpecCT]
c:645 [binder, in SpecCT]
c:669 [binder, in SpecCT]
c:682 [binder, in SpecCT]
c:706 [binder, in SpecCT]
c:709 [binder, in SpecCT]
c:712 [binder, in SpecCT]
c:715 [binder, in SpecCT]
c:719 [binder, in SpecCT]
c:726 [binder, in SpecCT]
c:736 [binder, in SpecCT]
c:756 [binder, in SpecCT]
c:768 [binder, in SpecCT]
c:780 [binder, in SpecCT]
c:787 [binder, in SpecCT]
c:797 [binder, in SpecCT]
c:801 [binder, in SpecCT]
c:862 [binder, in SpecCT]
c:883 [binder, in SpecCT]
c:886 [binder, in SpecCT]
c:896 [binder, in SpecCT]
c:910 [binder, in SpecCT]
D
dead_store_example [lemma, in RelHoare]DForce [constructor, in SpecCT]
different_code [lemma, in StaticIFC]
direction [inductive, in SpecCT]
dirs [definition, in SpecCT]
DLoad [constructor, in SpecCT]
dop:868 [binder, in SpecCT]
dop:873 [binder, in SpecCT]
dop:880 [binder, in SpecCT]
dsn:908 [binder, in SpecCT]
DStep [constructor, in SpecCT]
DStore [constructor, in SpecCT]
ds':718 [binder, in SpecCT]
ds':905 [binder, in SpecCT]
ds0:600 [binder, in SpecCT]
ds1':609 [binder, in SpecCT]
ds1':678 [binder, in SpecCT]
ds1:287 [binder, in SpecCT]
ds1:456 [binder, in SpecCT]
ds1:595 [binder, in SpecCT]
ds1:598 [binder, in SpecCT]
ds1:603 [binder, in SpecCT]
ds1:607 [binder, in SpecCT]
ds1:641 [binder, in SpecCT]
ds1:667 [binder, in SpecCT]
ds1:723 [binder, in SpecCT]
ds2':610 [binder, in SpecCT]
ds2':679 [binder, in SpecCT]
ds2:288 [binder, in SpecCT]
ds2:457 [binder, in SpecCT]
ds2:596 [binder, in SpecCT]
ds2:599 [binder, in SpecCT]
ds2:604 [binder, in SpecCT]
ds2:608 [binder, in SpecCT]
ds2:642 [binder, in SpecCT]
ds2:668 [binder, in SpecCT]
ds2:725 [binder, in SpecCT]
ds3:601 [binder, in SpecCT]
ds3:605 [binder, in SpecCT]
ds:299 [binder, in SpecCT]
ds:310 [binder, in SpecCT]
ds:315 [binder, in SpecCT]
ds:368 [binder, in SpecCT]
ds:375 [binder, in SpecCT]
ds:384 [binder, in SpecCT]
ds:393 [binder, in SpecCT]
ds:406 [binder, in SpecCT]
ds:468 [binder, in SpecCT]
ds:479 [binder, in SpecCT]
ds:484 [binder, in SpecCT]
ds:527 [binder, in SpecCT]
ds:538 [binder, in SpecCT]
ds:548 [binder, in SpecCT]
ds:561 [binder, in SpecCT]
ds:575 [binder, in SpecCT]
ds:577 [binder, in SpecCT]
ds:659 [binder, in SpecCT]
ds:696 [binder, in SpecCT]
ds:713 [binder, in SpecCT]
ds:716 [binder, in SpecCT]
ds:720 [binder, in SpecCT]
ds:727 [binder, in SpecCT]
ds:737 [binder, in SpecCT]
ds:755 [binder, in SpecCT]
ds:767 [binder, in SpecCT]
ds:779 [binder, in SpecCT]
ds:788 [binder, in SpecCT]
ds:798 [binder, in SpecCT]
ds:814 [binder, in SpecCT]
ds:884 [binder, in SpecCT]
ds:890 [binder, in SpecCT]
ds:900 [binder, in SpecCT]
ds:914 [binder, in SpecCT]
d1:109 [binder, in RelHoare]
d1:131 [binder, in RelHoare]
d1:137 [binder, in RelHoare]
d2:110 [binder, in RelHoare]
d2:132 [binder, in RelHoare]
d2:138 [binder, in RelHoare]
d:407 [binder, in SpecCT]
d:532 [binder, in SpecCT]
d:553 [binder, in SpecCT]
d:562 [binder, in SpecCT]
d:594 [binder, in SpecCT]
E
example1_sme_insecure_f [definition, in Noninterference]example1_secure_f [definition, in Noninterference]
example2_sme_insecure_f [definition, in Noninterference]
example2_secure_f [definition, in Noninterference]
example3_sme_insecure_f [definition, in Noninterference]
example3_secure_f [definition, in Noninterference]
E_While [constructor, in StaticIFC]
E_IfFalse [constructor, in StaticIFC]
E_IfTrue [constructor, in StaticIFC]
E_Seq [constructor, in StaticIFC]
E_Asgn [constructor, in StaticIFC]
E_Skip [constructor, in StaticIFC]
e1:165 [binder, in RelHoare]
e1:175 [binder, in RelHoare]
e1:187 [binder, in RelHoare]
e1:193 [binder, in RelHoare]
e2:166 [binder, in RelHoare]
e2:182 [binder, in RelHoare]
e2:200 [binder, in RelHoare]
e2:206 [binder, in RelHoare]
e:118 [binder, in SpecCT]
e:239 [binder, in SpecCT]
e:271 [binder, in SpecCT]
e:30 [binder, in SpecCT]
e:342 [binder, in SpecCT]
e:349 [binder, in SpecCT]
e:43 [binder, in SpecCT]
e:440 [binder, in SpecCT]
e:511 [binder, in SpecCT]
e:518 [binder, in SpecCT]
e:71 [binder, in SpecCT]
e:824 [binder, in SpecCT]
F
fact_iter_slow [definition, in RelHoare]fact_iter_fast [definition, in RelHoare]
FILL_IN_HERE [definition, in RelHoare]
FILL_IN_HERE [definition, in StaticIFC]
fuel:861 [binder, in SpecCT]
f:110 [binder, in Noninterference]
f:111 [binder, in Noninterference]
f:115 [binder, in Noninterference]
f:116 [binder, in Noninterference]
f:12 [binder, in Noninterference]
f:20 [binder, in Noninterference]
f:29 [binder, in Noninterference]
f:3 [binder, in Noninterference]
f:38 [binder, in Noninterference]
f:44 [binder, in RelHoare]
f:44 [binder, in Noninterference]
f:49 [binder, in RelHoare]
f:56 [binder, in Noninterference]
f:64 [binder, in Noninterference]
f:70 [binder, in Noninterference]
f:80 [binder, in Noninterference]
f:825 [binder, in SpecCT]
H
h1:579 [binder, in SpecCT]h1:584 [binder, in SpecCT]
h2:580 [binder, in SpecCT]
h2:585 [binder, in SpecCT]
I
ideal_unused_update_rev [lemma, in SpecCT]ideal_unused_update [lemma, in SpecCT]
ideal_unused_overwrite [lemma, in SpecCT]
ideal_spec_ct_secure [lemma, in SpecCT]
Ideal_Write_U [constructor, in SpecCT]
Ideal_Write [constructor, in SpecCT]
Ideal_ARead_U [constructor, in SpecCT]
Ideal_ARead [constructor, in SpecCT]
Ideal_While [constructor, in SpecCT]
Ideal_If_F [constructor, in SpecCT]
Ideal_If [constructor, in SpecCT]
Ideal_Seq [constructor, in SpecCT]
Ideal_Asgn [constructor, in SpecCT]
Ideal_Skip [constructor, in SpecCT]
ideal_eval [inductive, in SpecCT]
ie:111 [binder, in SpecCT]
ie:116 [binder, in SpecCT]
ie:326 [binder, in SpecCT]
ie:332 [binder, in SpecCT]
ie:340 [binder, in SpecCT]
ie:347 [binder, in SpecCT]
ie:495 [binder, in SpecCT]
ie:501 [binder, in SpecCT]
ie:509 [binder, in SpecCT]
ie:516 [binder, in SpecCT]
If [constructor, in SpecCT]
insecure_com2 [definition, in Noninterference]
insecure_com1 [definition, in Noninterference]
insecure_f [definition, in Noninterference]
insecure_com2 [definition, in StaticIFC]
insecure_com1 [definition, in StaticIFC]
interferent_secore_com2 [lemma, in Noninterference]
interferent_secore_com1 [lemma, in Noninterference]
interferent_insecure_f [lemma, in Noninterference]
interferent_insecure_com1 [definition, in StaticIFC]
i':335 [binder, in SpecCT]
i':352 [binder, in SpecCT]
i':504 [binder, in SpecCT]
i':521 [binder, in SpecCT]
i:112 [binder, in SpecCT]
i:117 [binder, in SpecCT]
i:236 [binder, in SpecCT]
i:238 [binder, in SpecCT]
i:260 [binder, in SpecCT]
i:262 [binder, in SpecCT]
i:327 [binder, in SpecCT]
i:333 [binder, in SpecCT]
i:341 [binder, in SpecCT]
i:348 [binder, in SpecCT]
i:399 [binder, in SpecCT]
i:40 [binder, in SpecCT]
i:42 [binder, in SpecCT]
i:496 [binder, in SpecCT]
i:502 [binder, in SpecCT]
i:510 [binder, in SpecCT]
i:517 [binder, in SpecCT]
i:52 [binder, in SpecCT]
i:62 [binder, in SpecCT]
i:64 [binder, in SpecCT]
i:870 [binder, in SpecCT]
i:876 [binder, in SpecCT]
J
join [definition, in SpecCT]join [definition, in StaticIFC]
join_public [lemma, in SpecCT]
join_secret_l [lemma, in StaticIFC]
join_public_r [lemma, in StaticIFC]
join_public_l [lemma, in StaticIFC]
join_public [lemma, in StaticIFC]
join_commutative [lemma, in StaticIFC]
L
label [definition, in SpecCT]label [definition, in StaticIFC]
label_of_bexp_unique [lemma, in StaticIFC]
label_of_bexp_sound [lemma, in StaticIFC]
label_of_bexp [definition, in StaticIFC]
label_of_aexp_unique [lemma, in StaticIFC]
label_of_aexp_sound [lemma, in StaticIFC]
label_of_aexp [definition, in StaticIFC]
l1:101 [binder, in StaticIFC]
l1:105 [binder, in StaticIFC]
l1:108 [binder, in StaticIFC]
l1:111 [binder, in StaticIFC]
l1:114 [binder, in StaticIFC]
l1:118 [binder, in StaticIFC]
l1:121 [binder, in StaticIFC]
l1:152 [binder, in SpecCT]
l1:154 [binder, in SpecCT]
l1:156 [binder, in SpecCT]
l1:166 [binder, in SpecCT]
l1:170 [binder, in SpecCT]
l1:174 [binder, in SpecCT]
l1:180 [binder, in SpecCT]
l1:184 [binder, in SpecCT]
l1:188 [binder, in SpecCT]
l1:192 [binder, in SpecCT]
l1:196 [binder, in SpecCT]
l1:202 [binder, in SpecCT]
l1:24 [binder, in StaticIFC]
l1:26 [binder, in StaticIFC]
l1:28 [binder, in StaticIFC]
l1:39 [binder, in StaticIFC]
l1:43 [binder, in StaticIFC]
l1:47 [binder, in StaticIFC]
l1:67 [binder, in StaticIFC]
l1:71 [binder, in StaticIFC]
l1:75 [binder, in StaticIFC]
l1:79 [binder, in StaticIFC]
l1:85 [binder, in StaticIFC]
l2:102 [binder, in StaticIFC]
l2:106 [binder, in StaticIFC]
l2:109 [binder, in StaticIFC]
l2:112 [binder, in StaticIFC]
l2:115 [binder, in StaticIFC]
l2:119 [binder, in StaticIFC]
l2:122 [binder, in StaticIFC]
l2:153 [binder, in SpecCT]
l2:155 [binder, in SpecCT]
l2:157 [binder, in SpecCT]
l2:168 [binder, in SpecCT]
l2:172 [binder, in SpecCT]
l2:176 [binder, in SpecCT]
l2:182 [binder, in SpecCT]
l2:186 [binder, in SpecCT]
l2:190 [binder, in SpecCT]
l2:194 [binder, in SpecCT]
l2:198 [binder, in SpecCT]
l2:204 [binder, in SpecCT]
l2:25 [binder, in StaticIFC]
l2:27 [binder, in StaticIFC]
l2:29 [binder, in StaticIFC]
l2:41 [binder, in StaticIFC]
l2:45 [binder, in StaticIFC]
l2:49 [binder, in StaticIFC]
l2:69 [binder, in StaticIFC]
l2:73 [binder, in StaticIFC]
l2:77 [binder, in StaticIFC]
l2:81 [binder, in StaticIFC]
l2:87 [binder, in StaticIFC]
l3:107 [binder, in StaticIFC]
l:103 [binder, in StaticIFC]
l:104 [binder, in StaticIFC]
l:110 [binder, in StaticIFC]
l:113 [binder, in StaticIFC]
l:116 [binder, in StaticIFC]
l:117 [binder, in StaticIFC]
l:120 [binder, in StaticIFC]
l:128 [binder, in StaticIFC]
l:153 [binder, in StaticIFC]
l:159 [binder, in StaticIFC]
l:164 [binder, in StaticIFC]
l:178 [binder, in SpecCT]
l:200 [binder, in SpecCT]
l:207 [binder, in StaticIFC]
l:209 [binder, in SpecCT]
l:211 [binder, in SpecCT]
l:213 [binder, in StaticIFC]
l:226 [binder, in SpecCT]
l:240 [binder, in SpecCT]
l:30 [binder, in StaticIFC]
l:31 [binder, in StaticIFC]
l:32 [binder, in StaticIFC]
l:58 [binder, in StaticIFC]
l:83 [binder, in StaticIFC]
l:96 [binder, in StaticIFC]
M
merge_state_pub_equiv [lemma, in Noninterference]merge_states_split_state [lemma, in Noninterference]
merge_states [definition, in Noninterference]
mf:92 [binder, in Noninterference]
mkAexp [abbreviation, in RelHoare]
ms:95 [binder, in Noninterference]
m:892 [binder, in SpecCT]
m:894 [binder, in SpecCT]
N
name:827 [binder, in SpecCT]name:830 [binder, in SpecCT]
name:835 [binder, in SpecCT]
name:838 [binder, in SpecCT]
new_ast:842 [binder, in SpecCT]
new_st:834 [binder, in SpecCT]
Noninterference [library]
noninterference_crossproduct [definition, in RelHoare]
noninterference_lockstep [definition, in RelHoare]
noninterferent [definition, in Noninterference]
noninterferent [definition, in StaticIFC]
noninterferent_bexp [lemma, in SpecCT]
noninterferent_aexp [lemma, in SpecCT]
noninterferent_aexp_bexp [lemma, in SpecCT]
noninterferent_while_sme [lemma, in Noninterference]
noninterferent_while_R [definition, in Noninterference]
noninterferent_secore_com' [lemma, in Noninterference]
noninterferent_while [definition, in Noninterference]
noninterferent_sme_insecure_com2 [lemma, in Noninterference]
noninterferent_sme_insecure_com1 [lemma, in Noninterference]
noninterferent_secore_com [lemma, in Noninterference]
noninterferent_no_while [definition, in Noninterference]
noninterferent_sme_state [lemma, in Noninterference]
noninterferent_state_ni [lemma, in Noninterference]
noninterferent_state [definition, in Noninterference]
noninterferent_sme [lemma, in Noninterference]
noninterferent_splittable [lemma, in Noninterference]
noninterferent_secure_f [lemma, in Noninterference]
noninterferent_bexp [lemma, in StaticIFC]
noninterferent_aexp [lemma, in StaticIFC]
noninterferent_secure_com [definition, in StaticIFC]
not_wt_insecure_com2 [definition, in StaticIFC]
not_swt_noninterferent_com_is_noninterferent [definition, in StaticIFC]
not_swt_noninterferent_com [definition, in StaticIFC]
not_swt_insecure_com2 [definition, in StaticIFC]
not_swt_insecure_com1 [definition, in StaticIFC]
ns:53 [binder, in SpecCT]
n:119 [binder, in SpecCT]
n:163 [binder, in SpecCT]
n:240 [binder, in StaticIFC]
n:272 [binder, in SpecCT]
n:343 [binder, in SpecCT]
n:350 [binder, in SpecCT]
n:36 [binder, in StaticIFC]
n:441 [binder, in SpecCT]
n:5 [binder, in SpecCT]
n:512 [binder, in SpecCT]
n:519 [binder, in SpecCT]
n:54 [binder, in SpecCT]
n:6 [binder, in RelHoare]
n:72 [binder, in SpecCT]
n:740 [binder, in SpecCT]
n:746 [binder, in SpecCT]
n:750 [binder, in SpecCT]
n:762 [binder, in SpecCT]
n:774 [binder, in SpecCT]
n:786 [binder, in SpecCT]
n:878 [binder, in SpecCT]
n:891 [binder, in SpecCT]
n:893 [binder, in SpecCT]
n:895 [binder, in SpecCT]
O
OARead [constructor, in SpecCT]OAWrite [constructor, in SpecCT]
OBranch [constructor, in SpecCT]
obs [definition, in SpecCT]
observation [inductive, in SpecCT]
osn:909 [binder, in SpecCT]
os':906 [binder, in SpecCT]
os':918 [binder, in SpecCT]
os1:148 [binder, in SpecCT]
os1:252 [binder, in SpecCT]
os1:285 [binder, in SpecCT]
os1:298 [binder, in SpecCT]
os1:309 [binder, in SpecCT]
os1:366 [binder, in SpecCT]
os1:425 [binder, in SpecCT]
os1:454 [binder, in SpecCT]
os1:467 [binder, in SpecCT]
os1:478 [binder, in SpecCT]
os1:639 [binder, in SpecCT]
os1:657 [binder, in SpecCT]
os1:676 [binder, in SpecCT]
os1:694 [binder, in SpecCT]
os1:812 [binder, in SpecCT]
os1:82 [binder, in SpecCT]
os1:91 [binder, in SpecCT]
os1:924 [binder, in SpecCT]
os1:932 [binder, in SpecCT]
os1:99 [binder, in SpecCT]
os2:149 [binder, in SpecCT]
os2:253 [binder, in SpecCT]
os2:286 [binder, in SpecCT]
os2:367 [binder, in SpecCT]
os2:426 [binder, in SpecCT]
os2:455 [binder, in SpecCT]
os2:640 [binder, in SpecCT]
os2:658 [binder, in SpecCT]
os2:677 [binder, in SpecCT]
os2:695 [binder, in SpecCT]
os2:813 [binder, in SpecCT]
os2:83 [binder, in SpecCT]
os2:928 [binder, in SpecCT]
os2:936 [binder, in SpecCT]
os:105 [binder, in SpecCT]
os:263 [binder, in StaticIFC]
os:319 [binder, in SpecCT]
os:379 [binder, in SpecCT]
os:388 [binder, in SpecCT]
os:397 [binder, in SpecCT]
os:405 [binder, in SpecCT]
os:413 [binder, in SpecCT]
os:488 [binder, in SpecCT]
os:531 [binder, in SpecCT]
os:542 [binder, in SpecCT]
os:552 [binder, in SpecCT]
os:560 [binder, in SpecCT]
os:569 [binder, in SpecCT]
os:735 [binder, in SpecCT]
os:760 [binder, in SpecCT]
os:772 [binder, in SpecCT]
os:784 [binder, in SpecCT]
os:796 [binder, in SpecCT]
os:901 [binder, in SpecCT]
o:855 [binder, in SpecCT]
P
PA:138 [binder, in SpecCT]PA:151 [binder, in SpecCT]
PA:221 [binder, in SpecCT]
PA:242 [binder, in SpecCT]
PA:255 [binder, in SpecCT]
PA:354 [binder, in SpecCT]
PA:370 [binder, in SpecCT]
PA:415 [binder, in SpecCT]
PA:626 [binder, in SpecCT]
PA:644 [binder, in SpecCT]
PA:661 [binder, in SpecCT]
PA:681 [binder, in SpecCT]
PA:800 [binder, in SpecCT]
PA:920 [binder, in SpecCT]
pceval [inductive, in StaticIFC]
pceval_ceval [lemma, in StaticIFC]
PCWT_While [constructor, in StaticIFC]
PCWT_If [constructor, in StaticIFC]
PCWT_Seq [constructor, in StaticIFC]
PCWT_Asgn [constructor, in StaticIFC]
PCWT_Com [constructor, in StaticIFC]
pc_well_typed_pc_secure [lemma, in StaticIFC]
pc_secure [definition, in StaticIFC]
pc_well_typed_noninterferent [lemma, in StaticIFC]
pc_typechecker_complete [lemma, in StaticIFC]
pc_typechecker_sound [lemma, in StaticIFC]
pc_typechecker [definition, in StaticIFC]
pc_well_typed [inductive, in StaticIFC]
pc1:178 [binder, in StaticIFC]
pc2:179 [binder, in StaticIFC]
pc:149 [binder, in StaticIFC]
pc:150 [binder, in StaticIFC]
pc:154 [binder, in StaticIFC]
pc:157 [binder, in StaticIFC]
pc:162 [binder, in StaticIFC]
pc:167 [binder, in StaticIFC]
pc:172 [binder, in StaticIFC]
pc:175 [binder, in StaticIFC]
pc:203 [binder, in StaticIFC]
pc:204 [binder, in StaticIFC]
pc:208 [binder, in StaticIFC]
pc:211 [binder, in StaticIFC]
pc:220 [binder, in StaticIFC]
pf:30 [binder, in Noninterference]
pi1:21 [binder, in Noninterference]
pi2:22 [binder, in Noninterference]
pi:1 [binder, in Noninterference]
pi:13 [binder, in Noninterference]
PI:16 [binder, in Noninterference]
PI:25 [binder, in Noninterference]
pi:32 [binder, in Noninterference]
PI:34 [binder, in Noninterference]
PI:39 [binder, in Noninterference]
pi:4 [binder, in Noninterference]
pi:45 [binder, in Noninterference]
pi:46 [binder, in Noninterference]
pi:47 [binder, in Noninterference]
pi:49 [binder, in Noninterference]
PI:51 [binder, in Noninterference]
pi:57 [binder, in Noninterference]
PI:59 [binder, in Noninterference]
pi:6 [binder, in Noninterference]
PI:65 [binder, in Noninterference]
pi:71 [binder, in Noninterference]
pi:73 [binder, in Noninterference]
PI:8 [binder, in Noninterference]
PO:10 [binder, in Noninterference]
PO:18 [binder, in Noninterference]
PO:27 [binder, in Noninterference]
PO:36 [binder, in Noninterference]
PO:41 [binder, in Noninterference]
PO:53 [binder, in Noninterference]
PO:61 [binder, in Noninterference]
PO:67 [binder, in Noninterference]
prefix [definition, in SpecCT]
prefix_append_front [lemma, in SpecCT]
prefix_app [lemma, in SpecCT]
prefix_cons [lemma, in SpecCT]
prefix_or_heads [lemma, in SpecCT]
prefix_heads [lemma, in SpecCT]
prefix_heads_and_tails [lemma, in SpecCT]
prefix_nil [lemma, in SpecCT]
prefix_refl [lemma, in SpecCT]
prog_size_monotonic [lemma, in SpecCT]
prog_size_ind [axiom, in SpecCT]
prog_size [definition, in SpecCT]
pst:821 [binder, in SpecCT]
pst:826 [binder, in SpecCT]
pst:828 [binder, in SpecCT]
pst:832 [binder, in SpecCT]
pst:836 [binder, in SpecCT]
pst:840 [binder, in SpecCT]
pst:843 [binder, in SpecCT]
pst:845 [binder, in SpecCT]
pst:848 [binder, in SpecCT]
pst:852 [binder, in SpecCT]
pst:856 [binder, in SpecCT]
pst:858 [binder, in SpecCT]
ps:139 [binder, in Noninterference]
ps:161 [binder, in Noninterference]
public [definition, in SpecCT]
public [definition, in StaticIFC]
pub_equiv_update_secret [lemma, in SpecCT]
pub_equiv_update_public [lemma, in SpecCT]
pub_equiv_trans [lemma, in SpecCT]
pub_equiv_sym [lemma, in SpecCT]
pub_equiv_refl [lemma, in SpecCT]
pub_equiv [definition, in SpecCT]
pub_arrs [definition, in SpecCT]
pub_vars [definition, in SpecCT]
pub_equiv_sym [lemma, in Noninterference]
pub_equiv_split_state [lemma, in Noninterference]
pub_equiv_merge_states [lemma, in Noninterference]
pub_equiv_split_iff [lemma, in Noninterference]
pub_equiv_split [definition, in Noninterference]
pub_equiv [definition, in Noninterference]
pub_map [definition, in Noninterference]
pub_equiv_trans [lemma, in StaticIFC]
pub_equiv_sym [lemma, in StaticIFC]
pub_equiv_refl [lemma, in StaticIFC]
pub_equiv [definition, in StaticIFC]
pub_vars [definition, in StaticIFC]
pub:100 [binder, in Noninterference]
pub:103 [binder, in Noninterference]
pub:108 [binder, in Noninterference]
pub:109 [binder, in Noninterference]
pub:112 [binder, in Noninterference]
pub:114 [binder, in Noninterference]
pub:117 [binder, in Noninterference]
pub:119 [binder, in Noninterference]
pub:129 [binder, in Noninterference]
pub:135 [binder, in Noninterference]
pub:142 [binder, in Noninterference]
pub:152 [binder, in Noninterference]
pub:154 [binder, in Noninterference]
pub:156 [binder, in Noninterference]
pub:159 [binder, in Noninterference]
pub:162 [binder, in Noninterference]
pub:167 [binder, in Noninterference]
pub:175 [binder, in Noninterference]
pub:177 [binder, in Noninterference]
pub:181 [binder, in Noninterference]
pub:75 [binder, in Noninterference]
pub:79 [binder, in Noninterference]
pub:84 [binder, in Noninterference]
pub:89 [binder, in Noninterference]
pub:91 [binder, in Noninterference]
pub:96 [binder, in Noninterference]
P':64 [binder, in RelHoare]
P':74 [binder, in RelHoare]
p1 [definition, in RelHoare]
p2 [definition, in RelHoare]
P:1 [binder, in RelHoare]
P:1 [binder, in StaticIFC]
P:10 [binder, in StaticIFC]
P:104 [binder, in RelHoare]
P:111 [binder, in RelHoare]
P:115 [binder, in RelHoare]
P:119 [binder, in RelHoare]
P:120 [binder, in SpecCT]
P:123 [binder, in RelHoare]
P:123 [binder, in StaticIFC]
P:126 [binder, in SpecCT]
P:127 [binder, in RelHoare]
P:129 [binder, in SpecCT]
P:133 [binder, in SpecCT]
P:133 [binder, in RelHoare]
P:136 [binder, in StaticIFC]
P:137 [binder, in SpecCT]
P:139 [binder, in RelHoare]
P:14 [binder, in StaticIFC]
P:140 [binder, in StaticIFC]
P:142 [binder, in StaticIFC]
P:144 [binder, in StaticIFC]
P:146 [binder, in StaticIFC]
P:150 [binder, in SpecCT]
P:158 [binder, in SpecCT]
P:159 [binder, in RelHoare]
P:166 [binder, in StaticIFC]
P:171 [binder, in RelHoare]
P:171 [binder, in StaticIFC]
P:174 [binder, in StaticIFC]
P:177 [binder, in RelHoare]
P:177 [binder, in StaticIFC]
P:18 [binder, in StaticIFC]
P:181 [binder, in StaticIFC]
P:183 [binder, in RelHoare]
P:185 [binder, in StaticIFC]
P:189 [binder, in RelHoare]
P:192 [binder, in StaticIFC]
P:194 [binder, in StaticIFC]
P:195 [binder, in RelHoare]
P:200 [binder, in StaticIFC]
P:201 [binder, in RelHoare]
P:205 [binder, in SpecCT]
P:207 [binder, in RelHoare]
P:212 [binder, in SpecCT]
P:212 [binder, in RelHoare]
P:215 [binder, in RelHoare]
P:216 [binder, in SpecCT]
P:218 [binder, in StaticIFC]
P:220 [binder, in SpecCT]
P:221 [binder, in StaticIFC]
P:223 [binder, in StaticIFC]
P:227 [binder, in StaticIFC]
P:233 [binder, in StaticIFC]
P:241 [binder, in SpecCT]
P:254 [binder, in SpecCT]
P:269 [binder, in StaticIFC]
P:277 [binder, in StaticIFC]
P:33 [binder, in StaticIFC]
P:353 [binder, in SpecCT]
P:369 [binder, in SpecCT]
P:414 [binder, in SpecCT]
P:427 [binder, in SpecCT]
P:431 [binder, in SpecCT]
P:5 [binder, in RelHoare]
P:50 [binder, in StaticIFC]
P:522 [binder, in SpecCT]
P:533 [binder, in SpecCT]
P:54 [binder, in RelHoare]
P:54 [binder, in StaticIFC]
P:543 [binder, in SpecCT]
P:554 [binder, in SpecCT]
P:56 [binder, in StaticIFC]
P:563 [binder, in SpecCT]
P:59 [binder, in StaticIFC]
P:611 [binder, in SpecCT]
P:618 [binder, in SpecCT]
P:62 [binder, in RelHoare]
P:625 [binder, in SpecCT]
P:63 [binder, in RelHoare]
P:63 [binder, in StaticIFC]
P:643 [binder, in SpecCT]
P:660 [binder, in SpecCT]
P:68 [binder, in RelHoare]
P:680 [binder, in SpecCT]
P:7 [binder, in StaticIFC]
P:714 [binder, in SpecCT]
P:728 [binder, in SpecCT]
P:73 [binder, in RelHoare]
P:751 [binder, in SpecCT]
P:763 [binder, in SpecCT]
P:775 [binder, in SpecCT]
P:789 [binder, in SpecCT]
P:799 [binder, in SpecCT]
P:81 [binder, in RelHoare]
P:86 [binder, in RelHoare]
P:88 [binder, in StaticIFC]
P:919 [binder, in SpecCT]
P:92 [binder, in StaticIFC]
P:94 [binder, in StaticIFC]
P:97 [binder, in StaticIFC]
Q
Q':70 [binder, in RelHoare]Q':76 [binder, in RelHoare]
Q:105 [binder, in RelHoare]
Q:112 [binder, in RelHoare]
Q:116 [binder, in RelHoare]
Q:120 [binder, in RelHoare]
Q:124 [binder, in RelHoare]
Q:128 [binder, in RelHoare]
Q:134 [binder, in RelHoare]
Q:140 [binder, in RelHoare]
Q:160 [binder, in RelHoare]
Q:172 [binder, in RelHoare]
Q:178 [binder, in RelHoare]
Q:184 [binder, in RelHoare]
Q:190 [binder, in RelHoare]
Q:196 [binder, in RelHoare]
Q:2 [binder, in RelHoare]
Q:202 [binder, in RelHoare]
Q:57 [binder, in RelHoare]
Q:65 [binder, in RelHoare]
Q:69 [binder, in RelHoare]
Q:75 [binder, in RelHoare]
Q:89 [binder, in RelHoare]
Q:94 [binder, in RelHoare]
Q:97 [binder, in RelHoare]
R
rassert [abbreviation, in RelHoare]RAssertion [definition, in RelHoare]
rassert_of_Prop [definition, in RelHoare]
rassert_implies [definition, in RelHoare]
RelHoare [library]
rhoare_while_2 [lemma, in RelHoare]
rhoare_while_1 [lemma, in RelHoare]
rhoare_while [lemma, in RelHoare]
rhoare_if_false_2 [lemma, in RelHoare]
rhoare_if_true_2 [lemma, in RelHoare]
rhoare_if_false_1 [lemma, in RelHoare]
rhoare_if_true_1 [lemma, in RelHoare]
rhoare_if_2 [lemma, in RelHoare]
rhoare_if_1 [lemma, in RelHoare]
rhoare_if [lemma, in RelHoare]
rhoare_equiv_skip_l_1' [lemma, in RelHoare]
rhoare_seq_2 [lemma, in RelHoare]
rhoare_seq_1 [lemma, in RelHoare]
rhoare_seq_skip_2 [lemma, in RelHoare]
rhoare_skip_seq_2 [lemma, in RelHoare]
rhoare_seq_skip_1 [lemma, in RelHoare]
rhoare_skip_seq_1 [lemma, in RelHoare]
rhoare_seq [lemma, in RelHoare]
rhoare_asgn_2 [lemma, in RelHoare]
rhoare_asgn_1 [lemma, in RelHoare]
rhoare_asgn [lemma, in RelHoare]
rhoare_consequence [lemma, in RelHoare]
rhoare_consequence_post [lemma, in RelHoare]
rhoare_consequence_pre [lemma, in RelHoare]
rhoare_skip [lemma, in RelHoare]
rhoare_judgment [definition, in RelHoare]
R:106 [binder, in RelHoare]
R:129 [binder, in RelHoare]
R:135 [binder, in RelHoare]
R:141 [binder, in Noninterference]
R:166 [binder, in Noninterference]
S
secret [definition, in SpecCT]secret [definition, in StaticIFC]
secret_run [lemma, in StaticIFC]
secure_com_noninterferent [lemma, in RelHoare]
secure_com_noninterferent_spec [definition, in RelHoare]
secure_com [definition, in RelHoare]
secure_com [definition, in Noninterference]
secure_f_rejected_again [lemma, in Noninterference]
secure_f [definition, in Noninterference]
secure_p2 [definition, in StaticIFC]
secure_com1' [definition, in StaticIFC]
secure_com [definition, in StaticIFC]
sel_slh_spec_ct_secure [lemma, in SpecCT]
sel_slh_ideal [lemma, in SpecCT]
sel_slh_ideal_prop [definition, in SpecCT]
sel_slh_flag [lemma, in SpecCT]
sel_slh_flag_prop [definition, in SpecCT]
sel_slh [definition, in SpecCT]
Seq [constructor, in SpecCT]
seq_spec_eval_ideal_eval [lemma, in SpecCT]
seq_ideal_eval [definition, in SpecCT]
seq_eval_ideal_eval_ind2 [lemma, in SpecCT]
seq_eval_ideal_eval_ind1 [lemma, in SpecCT]
seq_spec_eval [definition, in SpecCT]
sf:31 [binder, in Noninterference]
si1:14 [binder, in Noninterference]
si1:23 [binder, in Noninterference]
si2:15 [binder, in Noninterference]
si2:24 [binder, in Noninterference]
SI:17 [binder, in Noninterference]
si:2 [binder, in Noninterference]
SI:26 [binder, in Noninterference]
si:33 [binder, in Noninterference]
SI:35 [binder, in Noninterference]
SI:40 [binder, in Noninterference]
si:48 [binder, in Noninterference]
si:5 [binder, in Noninterference]
si:50 [binder, in Noninterference]
SI:52 [binder, in Noninterference]
si:58 [binder, in Noninterference]
SI:60 [binder, in Noninterference]
SI:66 [binder, in Noninterference]
si:7 [binder, in Noninterference]
si:72 [binder, in Noninterference]
si:74 [binder, in Noninterference]
SI:9 [binder, in Noninterference]
Skip [constructor, in SpecCT]
sme [definition, in Noninterference]
sme_while [definition, in Noninterference]
sme_insecure_com2 [definition, in Noninterference]
sme_insecure_com1 [definition, in Noninterference]
sme_cmd [definition, in Noninterference]
sme_state [definition, in Noninterference]
somewhat_transparent_while_sme [lemma, in Noninterference]
some_si:69 [binder, in Noninterference]
some_si:63 [binder, in Noninterference]
some_si:55 [binder, in Noninterference]
some_si:43 [binder, in Noninterference]
SO:11 [binder, in Noninterference]
SO:19 [binder, in Noninterference]
SO:28 [binder, in Noninterference]
SO:37 [binder, in Noninterference]
SO:42 [binder, in Noninterference]
SO:54 [binder, in Noninterference]
SO:62 [binder, in Noninterference]
SO:68 [binder, in Noninterference]
SpecCT [library]
SpecCTInterpreter [module, in SpecCT]
SpecCTInterpreter.bind [definition, in SpecCT]
SpecCTInterpreter.compute_fuel [definition, in SpecCT]
SpecCTInterpreter.eqb_reflect [lemma, in SpecCT]
SpecCTInterpreter.evaluator [definition, in SpecCT]
SpecCTInterpreter.eval_bexp [definition, in SpecCT]
SpecCTInterpreter.eval_aexp [definition, in SpecCT]
SpecCTInterpreter.fetch_direction [definition, in SpecCT]
SpecCTInterpreter.finish [definition, in SpecCT]
SpecCTInterpreter.get_arr [definition, in SpecCT]
SpecCTInterpreter.get_var [definition, in SpecCT]
SpecCTInterpreter.interpreter [definition, in SpecCT]
SpecCTInterpreter.is_speculating [definition, in SpecCT]
SpecCTInterpreter.ltb_reflect [lemma, in SpecCT]
SpecCTInterpreter.observe [definition, in SpecCT]
SpecCTInterpreter.OST_Finished [constructor, in SpecCT]
SpecCTInterpreter.OST_OutOfFuel [constructor, in SpecCT]
SpecCTInterpreter.OST_Error [constructor, in SpecCT]
SpecCTInterpreter.output_st [inductive, in SpecCT]
SpecCTInterpreter.prog_st [definition, in SpecCT]
SpecCTInterpreter.raise_error [definition, in SpecCT]
SpecCTInterpreter.ret [definition, in SpecCT]
SpecCTInterpreter.set_arr [definition, in SpecCT]
SpecCTInterpreter.set_var [definition, in SpecCT]
SpecCTInterpreter.spec_insecure_prog_2_is_ct_and_spec_insecure [definition, in SpecCT]
SpecCTInterpreter.spec_insecure_prog_2 [definition, in SpecCT]
SpecCTInterpreter.spec_eval_engine_sound [lemma, in SpecCT]
SpecCTInterpreter.spec_eval_engine_aux_sound [lemma, in SpecCT]
SpecCTInterpreter.spec_eval_engine [definition, in SpecCT]
SpecCTInterpreter.spec_eval_engine_aux [definition, in SpecCT]
SpecCTInterpreter.start_speculating [definition, in SpecCT]
_ >> _ [notation, in SpecCT]
_ >>= _ [notation, in SpecCT]
speculation_needs_force_ideal [lemma, in SpecCT]
speculation_needs_force [lemma, in SpecCT]
speculation_bit_monotonic [lemma, in SpecCT]
spec_insecure_prog_is_ct_and_spec_insecure [definition, in SpecCT]
spec_insecure_prog [definition, in SpecCT]
spec_ct_secure [definition, in SpecCT]
Spec_Write_U [constructor, in SpecCT]
Spec_Write [constructor, in SpecCT]
Spec_ARead_U [constructor, in SpecCT]
Spec_ARead [constructor, in SpecCT]
Spec_While [constructor, in SpecCT]
Spec_If_F [constructor, in SpecCT]
Spec_If [constructor, in SpecCT]
Spec_Seq [constructor, in SpecCT]
Spec_Asgn [constructor, in SpecCT]
Spec_Skip [constructor, in SpecCT]
spec_eval [inductive, in SpecCT]
splittable [definition, in Noninterference]
splittable_noninterferent [lemma, in Noninterference]
split_state_fun [definition, in Noninterference]
split_state [definition, in Noninterference]
ss:140 [binder, in Noninterference]
ss:160 [binder, in Noninterference]
state [definition, in SpecCT]
StaticIFC [library]
stt1:921 [binder, in SpecCT]
stt1:929 [binder, in SpecCT]
stt2:925 [binder, in SpecCT]
stt2:933 [binder, in SpecCT]
st'':246 [binder, in StaticIFC]
st'':282 [binder, in SpecCT]
st'':451 [binder, in SpecCT]
st'':80 [binder, in SpecCT]
st':103 [binder, in SpecCT]
st':245 [binder, in StaticIFC]
st':250 [binder, in StaticIFC]
st':256 [binder, in StaticIFC]
st':267 [binder, in StaticIFC]
st':279 [binder, in SpecCT]
st':292 [binder, in SpecCT]
st':303 [binder, in SpecCT]
st':316 [binder, in SpecCT]
st':403 [binder, in SpecCT]
st':411 [binder, in SpecCT]
st':448 [binder, in SpecCT]
st':461 [binder, in SpecCT]
st':472 [binder, in SpecCT]
st':485 [binder, in SpecCT]
st':732 [binder, in SpecCT]
st':757 [binder, in SpecCT]
st':769 [binder, in SpecCT]
st':78 [binder, in SpecCT]
st':781 [binder, in SpecCT]
st':793 [binder, in SpecCT]
st':86 [binder, in SpecCT]
st':902 [binder, in SpecCT]
st':915 [binder, in SpecCT]
st':94 [binder, in SpecCT]
st1':144 [binder, in SpecCT]
st1':360 [binder, in SpecCT]
st1':421 [binder, in SpecCT]
st1':60 [binder, in RelHoare]
st1':633 [binder, in SpecCT]
st1':806 [binder, in SpecCT]
st1:100 [binder, in RelHoare]
st1:102 [binder, in RelHoare]
st1:11 [binder, in RelHoare]
st1:13 [binder, in RelHoare]
st1:140 [binder, in SpecCT]
st1:144 [binder, in RelHoare]
st1:147 [binder, in RelHoare]
st1:149 [binder, in RelHoare]
st1:15 [binder, in RelHoare]
st1:150 [binder, in Noninterference]
st1:151 [binder, in RelHoare]
st1:154 [binder, in RelHoare]
st1:157 [binder, in RelHoare]
st1:167 [binder, in RelHoare]
st1:169 [binder, in RelHoare]
st1:17 [binder, in RelHoare]
st1:19 [binder, in RelHoare]
st1:21 [binder, in RelHoare]
st1:23 [binder, in RelHoare]
st1:25 [binder, in RelHoare]
st1:27 [binder, in RelHoare]
st1:29 [binder, in RelHoare]
st1:3 [binder, in RelHoare]
st1:31 [binder, in RelHoare]
st1:33 [binder, in RelHoare]
st1:35 [binder, in RelHoare]
st1:356 [binder, in SpecCT]
st1:37 [binder, in RelHoare]
st1:39 [binder, in RelHoare]
st1:41 [binder, in RelHoare]
st1:417 [binder, in SpecCT]
st1:46 [binder, in RelHoare]
st1:52 [binder, in RelHoare]
st1:58 [binder, in RelHoare]
st1:628 [binder, in SpecCT]
st1:670 [binder, in SpecCT]
st1:8 [binder, in RelHoare]
st1:802 [binder, in SpecCT]
st1:82 [binder, in RelHoare]
st1:87 [binder, in RelHoare]
st2':145 [binder, in SpecCT]
st2':361 [binder, in SpecCT]
st2':422 [binder, in SpecCT]
st2':61 [binder, in RelHoare]
st2':634 [binder, in SpecCT]
st2':807 [binder, in SpecCT]
st2:10 [binder, in RelHoare]
st2:101 [binder, in RelHoare]
st2:103 [binder, in RelHoare]
st2:12 [binder, in RelHoare]
st2:14 [binder, in RelHoare]
st2:141 [binder, in SpecCT]
st2:145 [binder, in RelHoare]
st2:148 [binder, in RelHoare]
st2:150 [binder, in RelHoare]
st2:151 [binder, in Noninterference]
st2:152 [binder, in RelHoare]
st2:155 [binder, in RelHoare]
st2:158 [binder, in RelHoare]
st2:16 [binder, in RelHoare]
st2:168 [binder, in RelHoare]
st2:170 [binder, in RelHoare]
st2:18 [binder, in RelHoare]
st2:20 [binder, in RelHoare]
st2:22 [binder, in RelHoare]
st2:24 [binder, in RelHoare]
st2:26 [binder, in RelHoare]
st2:28 [binder, in RelHoare]
st2:30 [binder, in RelHoare]
st2:32 [binder, in RelHoare]
st2:34 [binder, in RelHoare]
st2:357 [binder, in SpecCT]
st2:36 [binder, in RelHoare]
st2:38 [binder, in RelHoare]
st2:4 [binder, in RelHoare]
st2:40 [binder, in RelHoare]
st2:418 [binder, in SpecCT]
st2:42 [binder, in RelHoare]
st2:47 [binder, in RelHoare]
st2:53 [binder, in RelHoare]
st2:59 [binder, in RelHoare]
st2:629 [binder, in SpecCT]
st2:671 [binder, in SpecCT]
st2:803 [binder, in SpecCT]
st2:83 [binder, in RelHoare]
st2:88 [binder, in RelHoare]
st:101 [binder, in SpecCT]
st:107 [binder, in SpecCT]
st:113 [binder, in SpecCT]
st:149 [binder, in Noninterference]
st:237 [binder, in StaticIFC]
st:238 [binder, in StaticIFC]
st:244 [binder, in StaticIFC]
st:249 [binder, in StaticIFC]
st:255 [binder, in StaticIFC]
st:262 [binder, in StaticIFC]
st:265 [binder, in SpecCT]
st:266 [binder, in StaticIFC]
st:268 [binder, in SpecCT]
st:276 [binder, in SpecCT]
st:289 [binder, in SpecCT]
st:300 [binder, in SpecCT]
st:312 [binder, in SpecCT]
st:321 [binder, in SpecCT]
st:328 [binder, in SpecCT]
st:336 [binder, in SpecCT]
st:344 [binder, in SpecCT]
st:401 [binder, in SpecCT]
st:409 [binder, in SpecCT]
st:434 [binder, in SpecCT]
st:437 [binder, in SpecCT]
st:44 [binder, in SpecCT]
st:445 [binder, in SpecCT]
st:458 [binder, in SpecCT]
st:46 [binder, in SpecCT]
st:469 [binder, in SpecCT]
st:481 [binder, in SpecCT]
st:490 [binder, in SpecCT]
st:497 [binder, in SpecCT]
st:505 [binder, in SpecCT]
st:513 [binder, in SpecCT]
st:67 [binder, in SpecCT]
st:69 [binder, in SpecCT]
st:729 [binder, in SpecCT]
st:739 [binder, in SpecCT]
st:744 [binder, in SpecCT]
st:748 [binder, in SpecCT]
st:752 [binder, in SpecCT]
st:76 [binder, in SpecCT]
st:764 [binder, in SpecCT]
st:776 [binder, in SpecCT]
st:790 [binder, in SpecCT]
st:84 [binder, in SpecCT]
st:887 [binder, in SpecCT]
st:897 [binder, in SpecCT]
st:911 [binder, in SpecCT]
st:92 [binder, in SpecCT]
swap_equiv_spec [definition, in RelHoare]
swap_aux' [definition, in RelHoare]
swap_arith [definition, in RelHoare]
swap_aux [definition, in RelHoare]
swt_secure_com [definition, in StaticIFC]
s':138 [binder, in Noninterference]
s':165 [binder, in Noninterference]
s':180 [binder, in Noninterference]
s':184 [binder, in Noninterference]
s':184 [binder, in StaticIFC]
s':226 [binder, in StaticIFC]
s':376 [binder, in SpecCT]
s':385 [binder, in SpecCT]
s':394 [binder, in SpecCT]
s':528 [binder, in SpecCT]
s':539 [binder, in SpecCT]
s':549 [binder, in SpecCT]
s':558 [binder, in SpecCT]
s':567 [binder, in SpecCT]
s1':133 [binder, in Noninterference]
s1':146 [binder, in Noninterference]
s1':171 [binder, in Noninterference]
s1':190 [binder, in StaticIFC]
s1':198 [binder, in StaticIFC]
s1':22 [binder, in StaticIFC]
s1':231 [binder, in StaticIFC]
s1':248 [binder, in SpecCT]
s1':273 [binder, in StaticIFC]
s1':651 [binder, in SpecCT]
s1':688 [binder, in SpecCT]
s1:101 [binder, in Noninterference]
s1:11 [binder, in StaticIFC]
s1:122 [binder, in SpecCT]
s1:130 [binder, in SpecCT]
s1:131 [binder, in Noninterference]
s1:134 [binder, in SpecCT]
s1:144 [binder, in Noninterference]
s1:15 [binder, in StaticIFC]
s1:157 [binder, in Noninterference]
s1:169 [binder, in Noninterference]
s1:188 [binder, in StaticIFC]
s1:196 [binder, in StaticIFC]
s1:20 [binder, in StaticIFC]
s1:206 [binder, in SpecCT]
s1:213 [binder, in SpecCT]
s1:217 [binder, in SpecCT]
s1:229 [binder, in StaticIFC]
s1:244 [binder, in SpecCT]
s1:271 [binder, in StaticIFC]
s1:3 [binder, in StaticIFC]
s1:60 [binder, in StaticIFC]
s1:646 [binder, in SpecCT]
s1:662 [binder, in SpecCT]
s1:683 [binder, in SpecCT]
s1:76 [binder, in Noninterference]
s1:81 [binder, in Noninterference]
s1:87 [binder, in Noninterference]
s1:93 [binder, in Noninterference]
s1:97 [binder, in Noninterference]
s1:98 [binder, in StaticIFC]
s2':134 [binder, in Noninterference]
s2':147 [binder, in Noninterference]
s2':172 [binder, in Noninterference]
s2':191 [binder, in StaticIFC]
s2':199 [binder, in StaticIFC]
s2':23 [binder, in StaticIFC]
s2':232 [binder, in StaticIFC]
s2':249 [binder, in SpecCT]
s2':274 [binder, in StaticIFC]
s2':652 [binder, in SpecCT]
s2':689 [binder, in SpecCT]
s2:102 [binder, in Noninterference]
s2:12 [binder, in StaticIFC]
s2:123 [binder, in SpecCT]
s2:131 [binder, in SpecCT]
s2:132 [binder, in Noninterference]
s2:135 [binder, in SpecCT]
s2:145 [binder, in Noninterference]
s2:158 [binder, in Noninterference]
s2:16 [binder, in StaticIFC]
s2:170 [binder, in Noninterference]
s2:189 [binder, in StaticIFC]
s2:197 [binder, in StaticIFC]
s2:207 [binder, in SpecCT]
s2:21 [binder, in StaticIFC]
s2:214 [binder, in SpecCT]
s2:218 [binder, in SpecCT]
s2:230 [binder, in StaticIFC]
s2:245 [binder, in SpecCT]
s2:272 [binder, in StaticIFC]
s2:4 [binder, in StaticIFC]
s2:61 [binder, in StaticIFC]
s2:647 [binder, in SpecCT]
s2:663 [binder, in SpecCT]
s2:684 [binder, in SpecCT]
s2:77 [binder, in Noninterference]
s2:82 [binder, in Noninterference]
s2:88 [binder, in Noninterference]
s2:94 [binder, in Noninterference]
s2:98 [binder, in Noninterference]
s2:99 [binder, in StaticIFC]
s3:136 [binder, in SpecCT]
s3:17 [binder, in StaticIFC]
s:104 [binder, in Noninterference]
s:107 [binder, in Noninterference]
s:113 [binder, in Noninterference]
s:118 [binder, in Noninterference]
s:121 [binder, in Noninterference]
s:127 [binder, in SpecCT]
s:128 [binder, in Noninterference]
s:137 [binder, in Noninterference]
s:155 [binder, in Noninterference]
s:164 [binder, in Noninterference]
s:179 [binder, in Noninterference]
s:183 [binder, in Noninterference]
s:183 [binder, in StaticIFC]
s:225 [binder, in StaticIFC]
s:372 [binder, in SpecCT]
s:381 [binder, in SpecCT]
s:390 [binder, in SpecCT]
s:524 [binder, in SpecCT]
s:535 [binder, in SpecCT]
s:545 [binder, in SpecCT]
s:556 [binder, in SpecCT]
s:565 [binder, in SpecCT]
s:8 [binder, in StaticIFC]
s:83 [binder, in Noninterference]
T
terminating_noninterferent_tsni [lemma, in Noninterference]termination_leak [definition, in Noninterference]
tini_secure_termination_leak [definition, in Noninterference]
too_strong_def [definition, in Noninterference]
transparent_sme_state [lemma, in Noninterference]
transparent_sme [lemma, in Noninterference]
trivial_skip [definition, in RelHoare]
trivial_assignment_skip' [lemma, in RelHoare]
trivial_assignment_skip [lemma, in RelHoare]
tsni [definition, in StaticIFC]
tsni_transparent_while_sme [lemma, in Noninterference]
tsni_noninterferent [lemma, in Noninterference]
tsni_insecure_termination_leak [definition, in Noninterference]
tsni_while_R [definition, in Noninterference]
ts_well_typed_tsni [lemma, in StaticIFC]
ts_well_typed_equitermination [lemma, in StaticIFC]
ts_secret_run_terminating [lemma, in StaticIFC]
ts_well_typed_noninterferent [lemma, in StaticIFC]
ts_well_typed_well_typed [lemma, in StaticIFC]
TS_While [constructor, in StaticIFC]
TS_If [constructor, in StaticIFC]
TS_Seq [constructor, in StaticIFC]
TS_Asgn [constructor, in StaticIFC]
TS_Com [constructor, in StaticIFC]
ts_well_typed [inductive, in StaticIFC]
T_And [constructor, in SpecCT]
T_Not [constructor, in SpecCT]
T_Gt [constructor, in SpecCT]
T_Le [constructor, in SpecCT]
T_Neq [constructor, in SpecCT]
T_Eq [constructor, in SpecCT]
T_False [constructor, in SpecCT]
T_True [constructor, in SpecCT]
T_CTIf [constructor, in SpecCT]
T_Mult [constructor, in SpecCT]
T_Minus [constructor, in SpecCT]
T_Plus [constructor, in SpecCT]
T_Id [constructor, in SpecCT]
T_Num [constructor, in SpecCT]
T_And [constructor, in StaticIFC]
T_Not [constructor, in StaticIFC]
T_Gt [constructor, in StaticIFC]
T_Le [constructor, in StaticIFC]
T_Neq [constructor, in StaticIFC]
T_Eq [constructor, in StaticIFC]
T_False [constructor, in StaticIFC]
T_True [constructor, in StaticIFC]
T_Mult [constructor, in StaticIFC]
T_Minus [constructor, in StaticIFC]
T_Plus [constructor, in StaticIFC]
T_Id [constructor, in StaticIFC]
T_Num [constructor, in StaticIFC]
t1:163 [binder, in RelHoare]
t1:174 [binder, in RelHoare]
t1:186 [binder, in RelHoare]
t1:192 [binder, in RelHoare]
t1:581 [binder, in SpecCT]
t1:586 [binder, in SpecCT]
t1:613 [binder, in SpecCT]
t1:620 [binder, in SpecCT]
t2:164 [binder, in RelHoare]
t2:181 [binder, in RelHoare]
t2:199 [binder, in RelHoare]
t2:205 [binder, in RelHoare]
t2:582 [binder, in SpecCT]
t2:587 [binder, in SpecCT]
t2:614 [binder, in SpecCT]
t2:621 [binder, in SpecCT]
U
unsafe_access_needs_speculation [lemma, in SpecCT]unused [definition, in SpecCT]
upd [definition, in SpecCT]
u:907 [binder, in SpecCT]
V
value:820 [binder, in SpecCT]value:831 [binder, in SpecCT]
value:839 [binder, in SpecCT]
v:850 [binder, in SpecCT]
v:854 [binder, in SpecCT]
v:866 [binder, in SpecCT]
W
W [definition, in SpecCT]weaken_pc [lemma, in StaticIFC]
well_typed_noninterferent [lemma, in StaticIFC]
well_typed [inductive, in StaticIFC]
While [constructor, in SpecCT]
wt_noninterferent_com [definition, in StaticIFC]
wt_typechecker_complete [lemma, in StaticIFC]
wt_typechecker_sound [lemma, in StaticIFC]
wt_typechecker [definition, in StaticIFC]
WT_While [constructor, in StaticIFC]
WT_If [constructor, in StaticIFC]
WT_Seq [constructor, in StaticIFC]
WT_Asgn [constructor, in StaticIFC]
WT_Com [constructor, in StaticIFC]
X
X [definition, in SpecCT]xpub [definition, in Noninterference]
xpub [definition, in StaticIFC]
xpubX [lemma, in Noninterference]
xpub_true [lemma, in Noninterference]
xs:571 [binder, in SpecCT]
xs:591 [binder, in SpecCT]
X1:90 [binder, in RelHoare]
X2:91 [binder, in RelHoare]
x:109 [binder, in SpecCT]
X:121 [binder, in SpecCT]
x:122 [binder, in Noninterference]
x:123 [binder, in Noninterference]
x:124 [binder, in SpecCT]
x:124 [binder, in Noninterference]
X:125 [binder, in SpecCT]
x:125 [binder, in Noninterference]
x:126 [binder, in Noninterference]
X:126 [binder, in StaticIFC]
X:128 [binder, in SpecCT]
X:13 [binder, in StaticIFC]
X:132 [binder, in SpecCT]
X:151 [binder, in StaticIFC]
X:164 [binder, in SpecCT]
x:173 [binder, in Noninterference]
x:174 [binder, in Noninterference]
X:2 [binder, in StaticIFC]
X:205 [binder, in StaticIFC]
X:224 [binder, in SpecCT]
x:234 [binder, in SpecCT]
x:241 [binder, in StaticIFC]
x:273 [binder, in SpecCT]
x:29 [binder, in SpecCT]
x:324 [binder, in SpecCT]
x:330 [binder, in SpecCT]
X:37 [binder, in StaticIFC]
x:38 [binder, in SpecCT]
X:43 [binder, in RelHoare]
x:442 [binder, in SpecCT]
x:45 [binder, in RelHoare]
X:48 [binder, in RelHoare]
x:493 [binder, in SpecCT]
x:499 [binder, in SpecCT]
x:5 [binder, in StaticIFC]
x:50 [binder, in RelHoare]
X:570 [binder, in SpecCT]
X:574 [binder, in SpecCT]
X:576 [binder, in SpecCT]
X:578 [binder, in SpecCT]
X:583 [binder, in SpecCT]
X:588 [binder, in SpecCT]
x:589 [binder, in SpecCT]
X:593 [binder, in SpecCT]
X:597 [binder, in SpecCT]
x:6 [binder, in SpecCT]
X:6 [binder, in StaticIFC]
X:602 [binder, in SpecCT]
X:606 [binder, in SpecCT]
X:615 [binder, in SpecCT]
X:622 [binder, in SpecCT]
x:697 [binder, in SpecCT]
x:699 [binder, in SpecCT]
x:705 [binder, in SpecCT]
x:73 [binder, in SpecCT]
X:738 [binder, in SpecCT]
X:743 [binder, in SpecCT]
X:747 [binder, in SpecCT]
X:761 [binder, in SpecCT]
X:773 [binder, in SpecCT]
x:78 [binder, in Noninterference]
X:785 [binder, in SpecCT]
X:79 [binder, in RelHoare]
X:84 [binder, in RelHoare]
x:86 [binder, in Noninterference]
X:9 [binder, in StaticIFC]
x:90 [binder, in Noninterference]
X:95 [binder, in RelHoare]
X:98 [binder, in RelHoare]
x:99 [binder, in Noninterference]
Y
Y [definition, in SpecCT]ys:572 [binder, in SpecCT]
ys:592 [binder, in SpecCT]
Y_neq_X [lemma, in Noninterference]
y:51 [binder, in RelHoare]
y:590 [binder, in SpecCT]
Z
Z [definition, in SpecCT]zs:573 [binder, in SpecCT]
z1:105 [binder, in Noninterference]
z2:106 [binder, in Noninterference]
other
com:_ [ _ ] <- _ (com_scope) [notation, in SpecCT]com:_ <- _ [[ _ ]] (com_scope) [notation, in SpecCT]
com:while _ do _ end (com_scope) [notation, in SpecCT]
com:if _ then _ else _ end (com_scope) [notation, in SpecCT]
com:_ ; _ (com_scope) [notation, in SpecCT]
com:_ := _ (com_scope) [notation, in SpecCT]
com:skip (com_scope) [notation, in SpecCT]
com:_ _ .. _ (com_scope) [notation, in SpecCT]
com:_ (com_scope) [notation, in SpecCT]
com:( _ ) (com_scope) [notation, in SpecCT]
com:_ _ .. _ (com_scope) [notation, in SpecCT]
com:_ (com_scope) [notation, in SpecCT]
com:( _ ) (com_scope) [notation, in SpecCT]
com:_ && _ [notation, in SpecCT]
com:_ <> _ [notation, in SpecCT]
com:_ = _ [notation, in SpecCT]
com:_ > _ [notation, in SpecCT]
com:_ <= _ [notation, in SpecCT]
com:_ ? _ : _ [notation, in SpecCT]
com:_ * _ [notation, in SpecCT]
com:_ - _ [notation, in SpecCT]
com:_ + _ [notation, in SpecCT]
com:false [notation, in SpecCT]
com:true [notation, in SpecCT]
com:~ _ [notation, in SpecCT]
<{{ _ }}> (com_scope) [notation, in SpecCT]
<{ _ }> (com_scope) [notation, in SpecCT]
_ [ _ .2 ⊢> _ ] (hoare_spec_scope) [notation, in RelHoare]
_ [ _ .1 ⊢> _ ] (hoare_spec_scope) [notation, in RelHoare]
_ !2 (rassertion_scope) [notation, in RelHoare]
_ !1 (rassertion_scope) [notation, in RelHoare]
_ .2 (rassertion_scope) [notation, in RelHoare]
_ .1 (rassertion_scope) [notation, in RelHoare]
_ * _ (rassertion_scope) [notation, in RelHoare]
_ - _ (rassertion_scope) [notation, in RelHoare]
_ + _ (rassertion_scope) [notation, in RelHoare]
_ > _ (rassertion_scope) [notation, in RelHoare]
_ >= _ (rassertion_scope) [notation, in RelHoare]
_ < _ (rassertion_scope) [notation, in RelHoare]
_ <= _ (rassertion_scope) [notation, in RelHoare]
_ <> _ (rassertion_scope) [notation, in RelHoare]
_ = _ (rassertion_scope) [notation, in RelHoare]
_ <-> _ (rassertion_scope) [notation, in RelHoare]
_ -> _ (rassertion_scope) [notation, in RelHoare]
_ \/ _ (rassertion_scope) [notation, in RelHoare]
_ /\ _ (rassertion_scope) [notation, in RelHoare]
~ _ (rassertion_scope) [notation, in RelHoare]
⊢ _ ~~ _ : _ => _ (rhoare_spec_scope) [notation, in RelHoare]
_ <<->> _ (rhoare_spec_scope) [notation, in RelHoare]
_ ->> _ (rhoare_spec_scope) [notation, in RelHoare]
_ ⊢ <( _ , _ , _ , _ )> =[ _ ]=> <( _ , _ , _ , _ )> [notation, in SpecCT]
_ ;; _ ⊢ct- _ [notation, in SpecCT]
_ ⊢b- _ ∈ _ [notation, in SpecCT]
_ ⊢a- _ ∈ _ [notation, in SpecCT]
_ =[ _ ]=> _ , _ [notation, in StaticIFC]
_ ;; _ ⊢ts- _ [notation, in StaticIFC]
_ ;; _ |-- _ [notation, in StaticIFC]
_ ⊢pc- _ [notation, in StaticIFC]
_ ⊢b- _ ∈ _ [notation, in StaticIFC]
_ ⊢a- _ ∈ _ [notation, in StaticIFC]
false [notation, in SpecCT]
true [notation, in SpecCT]
<( _ , _ , _ , _ )> =[ _ ]=> <( _ , _ , _ , _ )> [notation, in SpecCT]
<( _ , _ )> =[ _ ]=> <( _ , _ , _ )> [notation, in SpecCT]
Notation Index
S
_ >> _ [in SpecCT]_ >>= _ [in SpecCT]
other
com:_ [ _ ] <- _ (com_scope) [in SpecCT]com:_ <- _ [[ _ ]] (com_scope) [in SpecCT]
com:while _ do _ end (com_scope) [in SpecCT]
com:if _ then _ else _ end (com_scope) [in SpecCT]
com:_ ; _ (com_scope) [in SpecCT]
com:_ := _ (com_scope) [in SpecCT]
com:skip (com_scope) [in SpecCT]
com:_ _ .. _ (com_scope) [in SpecCT]
com:_ (com_scope) [in SpecCT]
com:( _ ) (com_scope) [in SpecCT]
com:_ _ .. _ (com_scope) [in SpecCT]
com:_ (com_scope) [in SpecCT]
com:( _ ) (com_scope) [in SpecCT]
com:_ && _ [in SpecCT]
com:_ <> _ [in SpecCT]
com:_ = _ [in SpecCT]
com:_ > _ [in SpecCT]
com:_ <= _ [in SpecCT]
com:_ ? _ : _ [in SpecCT]
com:_ * _ [in SpecCT]
com:_ - _ [in SpecCT]
com:_ + _ [in SpecCT]
com:false [in SpecCT]
com:true [in SpecCT]
com:~ _ [in SpecCT]
<{{ _ }}> (com_scope) [in SpecCT]
<{ _ }> (com_scope) [in SpecCT]
_ [ _ .2 ⊢> _ ] (hoare_spec_scope) [in RelHoare]
_ [ _ .1 ⊢> _ ] (hoare_spec_scope) [in RelHoare]
_ !2 (rassertion_scope) [in RelHoare]
_ !1 (rassertion_scope) [in RelHoare]
_ .2 (rassertion_scope) [in RelHoare]
_ .1 (rassertion_scope) [in RelHoare]
_ * _ (rassertion_scope) [in RelHoare]
_ - _ (rassertion_scope) [in RelHoare]
_ + _ (rassertion_scope) [in RelHoare]
_ > _ (rassertion_scope) [in RelHoare]
_ >= _ (rassertion_scope) [in RelHoare]
_ < _ (rassertion_scope) [in RelHoare]
_ <= _ (rassertion_scope) [in RelHoare]
_ <> _ (rassertion_scope) [in RelHoare]
_ = _ (rassertion_scope) [in RelHoare]
_ <-> _ (rassertion_scope) [in RelHoare]
_ -> _ (rassertion_scope) [in RelHoare]
_ \/ _ (rassertion_scope) [in RelHoare]
_ /\ _ (rassertion_scope) [in RelHoare]
~ _ (rassertion_scope) [in RelHoare]
⊢ _ ~~ _ : _ => _ (rhoare_spec_scope) [in RelHoare]
_ <<->> _ (rhoare_spec_scope) [in RelHoare]
_ ->> _ (rhoare_spec_scope) [in RelHoare]
_ ⊢ <( _ , _ , _ , _ )> =[ _ ]=> <( _ , _ , _ , _ )> [in SpecCT]
_ ;; _ ⊢ct- _ [in SpecCT]
_ ⊢b- _ ∈ _ [in SpecCT]
_ ⊢a- _ ∈ _ [in SpecCT]
_ =[ _ ]=> _ , _ [in StaticIFC]
_ ;; _ ⊢ts- _ [in StaticIFC]
_ ;; _ |-- _ [in StaticIFC]
_ ⊢pc- _ [in StaticIFC]
_ ⊢b- _ ∈ _ [in StaticIFC]
_ ⊢a- _ ∈ _ [in StaticIFC]
false [in SpecCT]
true [in SpecCT]
<( _ , _ , _ , _ )> =[ _ ]=> <( _ , _ , _ , _ )> [in SpecCT]
<( _ , _ )> =[ _ ]=> <( _ , _ , _ )> [in SpecCT]
Binder Index
A
ae:741 [in SpecCT]ae:745 [in SpecCT]
arr_a':882 [in SpecCT]
arr_a:877 [in SpecCT]
arr_a':875 [in SpecCT]
arr_a:871 [in SpecCT]
astt1:922 [in SpecCT]
astt1:930 [in SpecCT]
astt2:926 [in SpecCT]
astt2:934 [in SpecCT]
ast'':283 [in SpecCT]
ast'':452 [in SpecCT]
ast'':81 [in SpecCT]
ast':104 [in SpecCT]
ast':280 [in SpecCT]
ast':293 [in SpecCT]
ast':304 [in SpecCT]
ast':317 [in SpecCT]
ast':404 [in SpecCT]
ast':412 [in SpecCT]
ast':449 [in SpecCT]
ast':462 [in SpecCT]
ast':473 [in SpecCT]
ast':486 [in SpecCT]
ast':733 [in SpecCT]
ast':758 [in SpecCT]
ast':770 [in SpecCT]
ast':782 [in SpecCT]
ast':79 [in SpecCT]
ast':794 [in SpecCT]
ast':87 [in SpecCT]
ast':903 [in SpecCT]
ast':916 [in SpecCT]
ast':95 [in SpecCT]
ast1':146 [in SpecCT]
ast1':362 [in SpecCT]
ast1':423 [in SpecCT]
ast1':635 [in SpecCT]
ast1':808 [in SpecCT]
ast1:142 [in SpecCT]
ast1:358 [in SpecCT]
ast1:419 [in SpecCT]
ast1:630 [in SpecCT]
ast1:672 [in SpecCT]
ast1:804 [in SpecCT]
ast2':147 [in SpecCT]
ast2':363 [in SpecCT]
ast2':424 [in SpecCT]
ast2':636 [in SpecCT]
ast2':809 [in SpecCT]
ast2:143 [in SpecCT]
ast2:359 [in SpecCT]
ast2:420 [in SpecCT]
ast2:631 [in SpecCT]
ast2:673 [in SpecCT]
ast2:805 [in SpecCT]
ast:102 [in SpecCT]
ast:108 [in SpecCT]
ast:114 [in SpecCT]
ast:266 [in SpecCT]
ast:269 [in SpecCT]
ast:277 [in SpecCT]
ast:290 [in SpecCT]
ast:301 [in SpecCT]
ast:313 [in SpecCT]
ast:322 [in SpecCT]
ast:329 [in SpecCT]
ast:337 [in SpecCT]
ast:345 [in SpecCT]
ast:402 [in SpecCT]
ast:410 [in SpecCT]
ast:435 [in SpecCT]
ast:438 [in SpecCT]
ast:446 [in SpecCT]
ast:459 [in SpecCT]
ast:470 [in SpecCT]
ast:482 [in SpecCT]
ast:491 [in SpecCT]
ast:498 [in SpecCT]
ast:506 [in SpecCT]
ast:514 [in SpecCT]
ast:68 [in SpecCT]
ast:70 [in SpecCT]
ast:730 [in SpecCT]
ast:753 [in SpecCT]
ast:765 [in SpecCT]
ast:77 [in SpecCT]
ast:777 [in SpecCT]
ast:791 [in SpecCT]
ast:85 [in SpecCT]
ast:888 [in SpecCT]
ast:898 [in SpecCT]
ast:912 [in SpecCT]
ast:93 [in SpecCT]
ax:398 [in SpecCT]
a':334 [in SpecCT]
a':351 [in SpecCT]
a':377 [in SpecCT]
a':386 [in SpecCT]
a':395 [in SpecCT]
a':503 [in SpecCT]
a':520 [in SpecCT]
a':529 [in SpecCT]
a':540 [in SpecCT]
a':550 [in SpecCT]
a':559 [in SpecCT]
a':568 [in SpecCT]
a1':250 [in SpecCT]
a1':653 [in SpecCT]
a1':690 [in SpecCT]
a1:11 [in SpecCT]
a1:14 [in SpecCT]
a1:16 [in SpecCT]
a1:165 [in SpecCT]
a1:169 [in SpecCT]
a1:173 [in SpecCT]
a1:179 [in SpecCT]
a1:18 [in SpecCT]
a1:183 [in SpecCT]
a1:187 [in SpecCT]
a1:191 [in SpecCT]
a1:195 [in SpecCT]
a1:20 [in SpecCT]
a1:22 [in SpecCT]
a1:246 [in SpecCT]
a1:38 [in StaticIFC]
a1:42 [in StaticIFC]
a1:46 [in StaticIFC]
a1:616 [in SpecCT]
a1:623 [in SpecCT]
a1:648 [in SpecCT]
a1:66 [in StaticIFC]
a1:664 [in SpecCT]
a1:685 [in SpecCT]
a1:7 [in SpecCT]
a1:70 [in StaticIFC]
a1:74 [in StaticIFC]
a1:78 [in StaticIFC]
a1:9 [in SpecCT]
a1:92 [in RelHoare]
a2':251 [in SpecCT]
a2':654 [in SpecCT]
a2':691 [in SpecCT]
a2:10 [in SpecCT]
a2:12 [in SpecCT]
a2:15 [in SpecCT]
a2:167 [in SpecCT]
a2:17 [in SpecCT]
a2:171 [in SpecCT]
a2:175 [in SpecCT]
a2:181 [in SpecCT]
a2:185 [in SpecCT]
a2:189 [in SpecCT]
a2:19 [in SpecCT]
a2:193 [in SpecCT]
a2:197 [in SpecCT]
a2:21 [in SpecCT]
a2:23 [in SpecCT]
a2:247 [in SpecCT]
a2:40 [in StaticIFC]
a2:44 [in StaticIFC]
a2:48 [in StaticIFC]
a2:617 [in SpecCT]
a2:624 [in SpecCT]
a2:649 [in SpecCT]
a2:665 [in SpecCT]
a2:68 [in StaticIFC]
a2:686 [in SpecCT]
a2:72 [in StaticIFC]
a2:76 [in StaticIFC]
a2:8 [in SpecCT]
a2:80 [in StaticIFC]
a2:93 [in RelHoare]
a:110 [in SpecCT]
a:115 [in SpecCT]
a:127 [in StaticIFC]
a:152 [in StaticIFC]
a:206 [in StaticIFC]
a:208 [in SpecCT]
a:215 [in SpecCT]
a:225 [in SpecCT]
a:235 [in SpecCT]
a:237 [in SpecCT]
a:239 [in StaticIFC]
a:259 [in SpecCT]
a:261 [in SpecCT]
a:325 [in SpecCT]
a:331 [in SpecCT]
a:339 [in SpecCT]
a:346 [in SpecCT]
a:373 [in SpecCT]
a:382 [in SpecCT]
a:39 [in SpecCT]
a:391 [in SpecCT]
a:41 [in SpecCT]
a:45 [in SpecCT]
a:494 [in SpecCT]
a:500 [in SpecCT]
a:508 [in SpecCT]
a:51 [in StaticIFC]
a:515 [in SpecCT]
a:525 [in SpecCT]
a:536 [in SpecCT]
a:546 [in SpecCT]
a:55 [in StaticIFC]
a:557 [in SpecCT]
a:566 [in SpecCT]
a:57 [in StaticIFC]
a:61 [in SpecCT]
A:612 [in SpecCT]
A:619 [in SpecCT]
a:62 [in StaticIFC]
a:63 [in SpecCT]
a:698 [in SpecCT]
a:7 [in RelHoare]
a:80 [in RelHoare]
A:815 [in SpecCT]
A:818 [in SpecCT]
A:819 [in SpecCT]
A:822 [in SpecCT]
a:847 [in SpecCT]
a:85 [in RelHoare]
a:89 [in StaticIFC]
a:9 [in RelHoare]
a:96 [in RelHoare]
a:99 [in RelHoare]
B
be:177 [in SpecCT]be:295 [in SpecCT]
be:306 [in SpecCT]
be:311 [in SpecCT]
be:33 [in SpecCT]
be:36 [in SpecCT]
be:464 [in SpecCT]
be:475 [in SpecCT]
be:480 [in SpecCT]
be:742 [in SpecCT]
be:749 [in SpecCT]
be:851 [in SpecCT]
bool_value:867 [in SpecCT]
bs1:247 [in StaticIFC]
bs1:254 [in StaticIFC]
bs1:260 [in StaticIFC]
bs1:275 [in StaticIFC]
bs2:248 [in StaticIFC]
bs2:276 [in StaticIFC]
bs:268 [in StaticIFC]
bt1:923 [in SpecCT]
bt1:931 [in SpecCT]
bt2:927 [in SpecCT]
bt2:935 [in SpecCT]
b'':284 [in SpecCT]
b'':453 [in SpecCT]
b':281 [in SpecCT]
b':294 [in SpecCT]
b':305 [in SpecCT]
b':318 [in SpecCT]
b':378 [in SpecCT]
b':387 [in SpecCT]
b':396 [in SpecCT]
b':450 [in SpecCT]
b':463 [in SpecCT]
b':474 [in SpecCT]
b':487 [in SpecCT]
b':530 [in SpecCT]
b':541 [in SpecCT]
b':551 [in SpecCT]
b':734 [in SpecCT]
b':759 [in SpecCT]
b':771 [in SpecCT]
b':783 [in SpecCT]
b':795 [in SpecCT]
b':904 [in SpecCT]
b':917 [in SpecCT]
b1':364 [in SpecCT]
b1':637 [in SpecCT]
b1':655 [in SpecCT]
b1':692 [in SpecCT]
b1':810 [in SpecCT]
b1:161 [in RelHoare]
b1:173 [in RelHoare]
b1:185 [in RelHoare]
b1:191 [in RelHoare]
b1:201 [in SpecCT]
b1:208 [in RelHoare]
b1:213 [in RelHoare]
b1:25 [in SpecCT]
b1:674 [in SpecCT]
b1:84 [in StaticIFC]
b2':365 [in SpecCT]
b2':638 [in SpecCT]
b2':656 [in SpecCT]
b2':693 [in SpecCT]
b2':811 [in SpecCT]
b2:162 [in RelHoare]
b2:180 [in RelHoare]
b2:198 [in RelHoare]
b2:203 [in SpecCT]
b2:204 [in RelHoare]
b2:209 [in RelHoare]
b2:216 [in RelHoare]
b2:26 [in SpecCT]
b2:675 [in SpecCT]
b2:86 [in StaticIFC]
b:100 [in SpecCT]
b:100 [in StaticIFC]
b:13 [in SpecCT]
b:131 [in StaticIFC]
b:134 [in StaticIFC]
b:143 [in RelHoare]
b:146 [in RelHoare]
b:153 [in RelHoare]
b:156 [in RelHoare]
b:158 [in StaticIFC]
b:163 [in StaticIFC]
b:199 [in SpecCT]
b:210 [in SpecCT]
b:212 [in StaticIFC]
b:216 [in StaticIFC]
b:219 [in SpecCT]
b:229 [in SpecCT]
b:232 [in SpecCT]
b:24 [in SpecCT]
b:251 [in StaticIFC]
b:257 [in StaticIFC]
b:261 [in StaticIFC]
b:267 [in SpecCT]
b:270 [in SpecCT]
b:278 [in SpecCT]
b:291 [in SpecCT]
b:302 [in SpecCT]
b:314 [in SpecCT]
b:323 [in SpecCT]
b:338 [in SpecCT]
b:374 [in SpecCT]
b:383 [in SpecCT]
b:392 [in SpecCT]
b:436 [in SpecCT]
b:439 [in SpecCT]
b:447 [in SpecCT]
b:460 [in SpecCT]
b:47 [in SpecCT]
b:471 [in SpecCT]
b:483 [in SpecCT]
b:492 [in SpecCT]
b:507 [in SpecCT]
b:526 [in SpecCT]
b:537 [in SpecCT]
b:547 [in SpecCT]
b:60 [in SpecCT]
b:632 [in SpecCT]
b:650 [in SpecCT]
b:666 [in SpecCT]
b:687 [in SpecCT]
b:700 [in SpecCT]
b:731 [in SpecCT]
b:754 [in SpecCT]
b:766 [in SpecCT]
b:778 [in SpecCT]
b:792 [in SpecCT]
b:82 [in StaticIFC]
B:823 [in SpecCT]
b:85 [in Noninterference]
b:872 [in SpecCT]
b:879 [in SpecCT]
b:88 [in SpecCT]
b:889 [in SpecCT]
b:899 [in SpecCT]
b:913 [in SpecCT]
b:93 [in StaticIFC]
b:95 [in StaticIFC]
b:96 [in SpecCT]
C
c':717 [in SpecCT]c1:107 [in RelHoare]
c1:113 [in RelHoare]
c1:117 [in RelHoare]
c1:121 [in RelHoare]
c1:125 [in RelHoare]
c1:129 [in StaticIFC]
c1:130 [in RelHoare]
c1:132 [in StaticIFC]
c1:135 [in StaticIFC]
c1:141 [in RelHoare]
c1:155 [in StaticIFC]
c1:160 [in StaticIFC]
c1:165 [in StaticIFC]
c1:179 [in RelHoare]
c1:186 [in StaticIFC]
c1:197 [in RelHoare]
c1:203 [in RelHoare]
c1:209 [in StaticIFC]
c1:210 [in RelHoare]
c1:214 [in RelHoare]
c1:214 [in StaticIFC]
c1:217 [in StaticIFC]
c1:227 [in SpecCT]
c1:230 [in SpecCT]
c1:233 [in SpecCT]
c1:242 [in StaticIFC]
c1:252 [in StaticIFC]
c1:258 [in StaticIFC]
c1:274 [in SpecCT]
c1:296 [in SpecCT]
c1:307 [in SpecCT]
c1:31 [in SpecCT]
c1:34 [in SpecCT]
c1:443 [in SpecCT]
c1:465 [in SpecCT]
c1:476 [in SpecCT]
c1:55 [in RelHoare]
c1:66 [in RelHoare]
c1:71 [in RelHoare]
c1:722 [in SpecCT]
c1:74 [in SpecCT]
c1:77 [in RelHoare]
c1:89 [in SpecCT]
c1:97 [in SpecCT]
c2:108 [in RelHoare]
c2:114 [in RelHoare]
c2:118 [in RelHoare]
c2:122 [in RelHoare]
c2:126 [in RelHoare]
c2:130 [in StaticIFC]
c2:133 [in StaticIFC]
c2:136 [in RelHoare]
c2:142 [in RelHoare]
c2:156 [in StaticIFC]
c2:161 [in StaticIFC]
c2:176 [in RelHoare]
c2:187 [in StaticIFC]
c2:188 [in RelHoare]
c2:194 [in RelHoare]
c2:210 [in StaticIFC]
c2:211 [in RelHoare]
c2:215 [in StaticIFC]
c2:217 [in RelHoare]
c2:228 [in SpecCT]
c2:231 [in SpecCT]
c2:243 [in StaticIFC]
c2:253 [in StaticIFC]
c2:259 [in StaticIFC]
c2:275 [in SpecCT]
c2:297 [in SpecCT]
c2:308 [in SpecCT]
c2:32 [in SpecCT]
c2:35 [in SpecCT]
c2:444 [in SpecCT]
c2:466 [in SpecCT]
c2:477 [in SpecCT]
c2:56 [in RelHoare]
c2:67 [in RelHoare]
c2:72 [in RelHoare]
c2:724 [in SpecCT]
c2:75 [in SpecCT]
c2:78 [in RelHoare]
c2:90 [in SpecCT]
c2:98 [in SpecCT]
c:106 [in SpecCT]
c:120 [in Noninterference]
c:127 [in Noninterference]
c:130 [in Noninterference]
c:136 [in Noninterference]
c:137 [in StaticIFC]
c:139 [in SpecCT]
c:141 [in StaticIFC]
c:143 [in Noninterference]
c:143 [in StaticIFC]
c:145 [in StaticIFC]
c:148 [in Noninterference]
c:153 [in Noninterference]
c:163 [in Noninterference]
c:168 [in Noninterference]
c:168 [in StaticIFC]
c:173 [in StaticIFC]
c:176 [in Noninterference]
c:176 [in StaticIFC]
c:178 [in Noninterference]
c:180 [in StaticIFC]
c:182 [in Noninterference]
c:182 [in StaticIFC]
c:19 [in StaticIFC]
c:193 [in StaticIFC]
c:195 [in StaticIFC]
c:219 [in StaticIFC]
c:222 [in StaticIFC]
c:224 [in StaticIFC]
c:228 [in StaticIFC]
c:234 [in StaticIFC]
c:243 [in SpecCT]
c:256 [in SpecCT]
c:264 [in StaticIFC]
c:265 [in StaticIFC]
c:270 [in StaticIFC]
c:278 [in StaticIFC]
c:320 [in SpecCT]
c:355 [in SpecCT]
c:37 [in SpecCT]
c:371 [in SpecCT]
c:380 [in SpecCT]
c:389 [in SpecCT]
c:400 [in SpecCT]
c:408 [in SpecCT]
c:416 [in SpecCT]
c:428 [in SpecCT]
c:489 [in SpecCT]
c:523 [in SpecCT]
c:534 [in SpecCT]
c:544 [in SpecCT]
c:555 [in SpecCT]
c:564 [in SpecCT]
c:627 [in SpecCT]
c:645 [in SpecCT]
c:669 [in SpecCT]
c:682 [in SpecCT]
c:706 [in SpecCT]
c:709 [in SpecCT]
c:712 [in SpecCT]
c:715 [in SpecCT]
c:719 [in SpecCT]
c:726 [in SpecCT]
c:736 [in SpecCT]
c:756 [in SpecCT]
c:768 [in SpecCT]
c:780 [in SpecCT]
c:787 [in SpecCT]
c:797 [in SpecCT]
c:801 [in SpecCT]
c:862 [in SpecCT]
c:883 [in SpecCT]
c:886 [in SpecCT]
c:896 [in SpecCT]
c:910 [in SpecCT]
D
dop:868 [in SpecCT]dop:873 [in SpecCT]
dop:880 [in SpecCT]
dsn:908 [in SpecCT]
ds':718 [in SpecCT]
ds':905 [in SpecCT]
ds0:600 [in SpecCT]
ds1':609 [in SpecCT]
ds1':678 [in SpecCT]
ds1:287 [in SpecCT]
ds1:456 [in SpecCT]
ds1:595 [in SpecCT]
ds1:598 [in SpecCT]
ds1:603 [in SpecCT]
ds1:607 [in SpecCT]
ds1:641 [in SpecCT]
ds1:667 [in SpecCT]
ds1:723 [in SpecCT]
ds2':610 [in SpecCT]
ds2':679 [in SpecCT]
ds2:288 [in SpecCT]
ds2:457 [in SpecCT]
ds2:596 [in SpecCT]
ds2:599 [in SpecCT]
ds2:604 [in SpecCT]
ds2:608 [in SpecCT]
ds2:642 [in SpecCT]
ds2:668 [in SpecCT]
ds2:725 [in SpecCT]
ds3:601 [in SpecCT]
ds3:605 [in SpecCT]
ds:299 [in SpecCT]
ds:310 [in SpecCT]
ds:315 [in SpecCT]
ds:368 [in SpecCT]
ds:375 [in SpecCT]
ds:384 [in SpecCT]
ds:393 [in SpecCT]
ds:406 [in SpecCT]
ds:468 [in SpecCT]
ds:479 [in SpecCT]
ds:484 [in SpecCT]
ds:527 [in SpecCT]
ds:538 [in SpecCT]
ds:548 [in SpecCT]
ds:561 [in SpecCT]
ds:575 [in SpecCT]
ds:577 [in SpecCT]
ds:659 [in SpecCT]
ds:696 [in SpecCT]
ds:713 [in SpecCT]
ds:716 [in SpecCT]
ds:720 [in SpecCT]
ds:727 [in SpecCT]
ds:737 [in SpecCT]
ds:755 [in SpecCT]
ds:767 [in SpecCT]
ds:779 [in SpecCT]
ds:788 [in SpecCT]
ds:798 [in SpecCT]
ds:814 [in SpecCT]
ds:884 [in SpecCT]
ds:890 [in SpecCT]
ds:900 [in SpecCT]
ds:914 [in SpecCT]
d1:109 [in RelHoare]
d1:131 [in RelHoare]
d1:137 [in RelHoare]
d2:110 [in RelHoare]
d2:132 [in RelHoare]
d2:138 [in RelHoare]
d:407 [in SpecCT]
d:532 [in SpecCT]
d:553 [in SpecCT]
d:562 [in SpecCT]
d:594 [in SpecCT]
E
e1:165 [in RelHoare]e1:175 [in RelHoare]
e1:187 [in RelHoare]
e1:193 [in RelHoare]
e2:166 [in RelHoare]
e2:182 [in RelHoare]
e2:200 [in RelHoare]
e2:206 [in RelHoare]
e:118 [in SpecCT]
e:239 [in SpecCT]
e:271 [in SpecCT]
e:30 [in SpecCT]
e:342 [in SpecCT]
e:349 [in SpecCT]
e:43 [in SpecCT]
e:440 [in SpecCT]
e:511 [in SpecCT]
e:518 [in SpecCT]
e:71 [in SpecCT]
e:824 [in SpecCT]
F
fuel:861 [in SpecCT]f:110 [in Noninterference]
f:111 [in Noninterference]
f:115 [in Noninterference]
f:116 [in Noninterference]
f:12 [in Noninterference]
f:20 [in Noninterference]
f:29 [in Noninterference]
f:3 [in Noninterference]
f:38 [in Noninterference]
f:44 [in RelHoare]
f:44 [in Noninterference]
f:49 [in RelHoare]
f:56 [in Noninterference]
f:64 [in Noninterference]
f:70 [in Noninterference]
f:80 [in Noninterference]
f:825 [in SpecCT]
H
h1:579 [in SpecCT]h1:584 [in SpecCT]
h2:580 [in SpecCT]
h2:585 [in SpecCT]
I
ie:111 [in SpecCT]ie:116 [in SpecCT]
ie:326 [in SpecCT]
ie:332 [in SpecCT]
ie:340 [in SpecCT]
ie:347 [in SpecCT]
ie:495 [in SpecCT]
ie:501 [in SpecCT]
ie:509 [in SpecCT]
ie:516 [in SpecCT]
i':335 [in SpecCT]
i':352 [in SpecCT]
i':504 [in SpecCT]
i':521 [in SpecCT]
i:112 [in SpecCT]
i:117 [in SpecCT]
i:236 [in SpecCT]
i:238 [in SpecCT]
i:260 [in SpecCT]
i:262 [in SpecCT]
i:327 [in SpecCT]
i:333 [in SpecCT]
i:341 [in SpecCT]
i:348 [in SpecCT]
i:399 [in SpecCT]
i:40 [in SpecCT]
i:42 [in SpecCT]
i:496 [in SpecCT]
i:502 [in SpecCT]
i:510 [in SpecCT]
i:517 [in SpecCT]
i:52 [in SpecCT]
i:62 [in SpecCT]
i:64 [in SpecCT]
i:870 [in SpecCT]
i:876 [in SpecCT]
L
l1:101 [in StaticIFC]l1:105 [in StaticIFC]
l1:108 [in StaticIFC]
l1:111 [in StaticIFC]
l1:114 [in StaticIFC]
l1:118 [in StaticIFC]
l1:121 [in StaticIFC]
l1:152 [in SpecCT]
l1:154 [in SpecCT]
l1:156 [in SpecCT]
l1:166 [in SpecCT]
l1:170 [in SpecCT]
l1:174 [in SpecCT]
l1:180 [in SpecCT]
l1:184 [in SpecCT]
l1:188 [in SpecCT]
l1:192 [in SpecCT]
l1:196 [in SpecCT]
l1:202 [in SpecCT]
l1:24 [in StaticIFC]
l1:26 [in StaticIFC]
l1:28 [in StaticIFC]
l1:39 [in StaticIFC]
l1:43 [in StaticIFC]
l1:47 [in StaticIFC]
l1:67 [in StaticIFC]
l1:71 [in StaticIFC]
l1:75 [in StaticIFC]
l1:79 [in StaticIFC]
l1:85 [in StaticIFC]
l2:102 [in StaticIFC]
l2:106 [in StaticIFC]
l2:109 [in StaticIFC]
l2:112 [in StaticIFC]
l2:115 [in StaticIFC]
l2:119 [in StaticIFC]
l2:122 [in StaticIFC]
l2:153 [in SpecCT]
l2:155 [in SpecCT]
l2:157 [in SpecCT]
l2:168 [in SpecCT]
l2:172 [in SpecCT]
l2:176 [in SpecCT]
l2:182 [in SpecCT]
l2:186 [in SpecCT]
l2:190 [in SpecCT]
l2:194 [in SpecCT]
l2:198 [in SpecCT]
l2:204 [in SpecCT]
l2:25 [in StaticIFC]
l2:27 [in StaticIFC]
l2:29 [in StaticIFC]
l2:41 [in StaticIFC]
l2:45 [in StaticIFC]
l2:49 [in StaticIFC]
l2:69 [in StaticIFC]
l2:73 [in StaticIFC]
l2:77 [in StaticIFC]
l2:81 [in StaticIFC]
l2:87 [in StaticIFC]
l3:107 [in StaticIFC]
l:103 [in StaticIFC]
l:104 [in StaticIFC]
l:110 [in StaticIFC]
l:113 [in StaticIFC]
l:116 [in StaticIFC]
l:117 [in StaticIFC]
l:120 [in StaticIFC]
l:128 [in StaticIFC]
l:153 [in StaticIFC]
l:159 [in StaticIFC]
l:164 [in StaticIFC]
l:178 [in SpecCT]
l:200 [in SpecCT]
l:207 [in StaticIFC]
l:209 [in SpecCT]
l:211 [in SpecCT]
l:213 [in StaticIFC]
l:226 [in SpecCT]
l:240 [in SpecCT]
l:30 [in StaticIFC]
l:31 [in StaticIFC]
l:32 [in StaticIFC]
l:58 [in StaticIFC]
l:83 [in StaticIFC]
l:96 [in StaticIFC]
M
mf:92 [in Noninterference]ms:95 [in Noninterference]
m:892 [in SpecCT]
m:894 [in SpecCT]
N
name:827 [in SpecCT]name:830 [in SpecCT]
name:835 [in SpecCT]
name:838 [in SpecCT]
new_ast:842 [in SpecCT]
new_st:834 [in SpecCT]
ns:53 [in SpecCT]
n:119 [in SpecCT]
n:163 [in SpecCT]
n:240 [in StaticIFC]
n:272 [in SpecCT]
n:343 [in SpecCT]
n:350 [in SpecCT]
n:36 [in StaticIFC]
n:441 [in SpecCT]
n:5 [in SpecCT]
n:512 [in SpecCT]
n:519 [in SpecCT]
n:54 [in SpecCT]
n:6 [in RelHoare]
n:72 [in SpecCT]
n:740 [in SpecCT]
n:746 [in SpecCT]
n:750 [in SpecCT]
n:762 [in SpecCT]
n:774 [in SpecCT]
n:786 [in SpecCT]
n:878 [in SpecCT]
n:891 [in SpecCT]
n:893 [in SpecCT]
n:895 [in SpecCT]
O
osn:909 [in SpecCT]os':906 [in SpecCT]
os':918 [in SpecCT]
os1:148 [in SpecCT]
os1:252 [in SpecCT]
os1:285 [in SpecCT]
os1:298 [in SpecCT]
os1:309 [in SpecCT]
os1:366 [in SpecCT]
os1:425 [in SpecCT]
os1:454 [in SpecCT]
os1:467 [in SpecCT]
os1:478 [in SpecCT]
os1:639 [in SpecCT]
os1:657 [in SpecCT]
os1:676 [in SpecCT]
os1:694 [in SpecCT]
os1:812 [in SpecCT]
os1:82 [in SpecCT]
os1:91 [in SpecCT]
os1:924 [in SpecCT]
os1:932 [in SpecCT]
os1:99 [in SpecCT]
os2:149 [in SpecCT]
os2:253 [in SpecCT]
os2:286 [in SpecCT]
os2:367 [in SpecCT]
os2:426 [in SpecCT]
os2:455 [in SpecCT]
os2:640 [in SpecCT]
os2:658 [in SpecCT]
os2:677 [in SpecCT]
os2:695 [in SpecCT]
os2:813 [in SpecCT]
os2:83 [in SpecCT]
os2:928 [in SpecCT]
os2:936 [in SpecCT]
os:105 [in SpecCT]
os:263 [in StaticIFC]
os:319 [in SpecCT]
os:379 [in SpecCT]
os:388 [in SpecCT]
os:397 [in SpecCT]
os:405 [in SpecCT]
os:413 [in SpecCT]
os:488 [in SpecCT]
os:531 [in SpecCT]
os:542 [in SpecCT]
os:552 [in SpecCT]
os:560 [in SpecCT]
os:569 [in SpecCT]
os:735 [in SpecCT]
os:760 [in SpecCT]
os:772 [in SpecCT]
os:784 [in SpecCT]
os:796 [in SpecCT]
os:901 [in SpecCT]
o:855 [in SpecCT]
P
PA:138 [in SpecCT]PA:151 [in SpecCT]
PA:221 [in SpecCT]
PA:242 [in SpecCT]
PA:255 [in SpecCT]
PA:354 [in SpecCT]
PA:370 [in SpecCT]
PA:415 [in SpecCT]
PA:626 [in SpecCT]
PA:644 [in SpecCT]
PA:661 [in SpecCT]
PA:681 [in SpecCT]
PA:800 [in SpecCT]
PA:920 [in SpecCT]
pc1:178 [in StaticIFC]
pc2:179 [in StaticIFC]
pc:149 [in StaticIFC]
pc:150 [in StaticIFC]
pc:154 [in StaticIFC]
pc:157 [in StaticIFC]
pc:162 [in StaticIFC]
pc:167 [in StaticIFC]
pc:172 [in StaticIFC]
pc:175 [in StaticIFC]
pc:203 [in StaticIFC]
pc:204 [in StaticIFC]
pc:208 [in StaticIFC]
pc:211 [in StaticIFC]
pc:220 [in StaticIFC]
pf:30 [in Noninterference]
pi1:21 [in Noninterference]
pi2:22 [in Noninterference]
pi:1 [in Noninterference]
pi:13 [in Noninterference]
PI:16 [in Noninterference]
PI:25 [in Noninterference]
pi:32 [in Noninterference]
PI:34 [in Noninterference]
PI:39 [in Noninterference]
pi:4 [in Noninterference]
pi:45 [in Noninterference]
pi:46 [in Noninterference]
pi:47 [in Noninterference]
pi:49 [in Noninterference]
PI:51 [in Noninterference]
pi:57 [in Noninterference]
PI:59 [in Noninterference]
pi:6 [in Noninterference]
PI:65 [in Noninterference]
pi:71 [in Noninterference]
pi:73 [in Noninterference]
PI:8 [in Noninterference]
PO:10 [in Noninterference]
PO:18 [in Noninterference]
PO:27 [in Noninterference]
PO:36 [in Noninterference]
PO:41 [in Noninterference]
PO:53 [in Noninterference]
PO:61 [in Noninterference]
PO:67 [in Noninterference]
pst:821 [in SpecCT]
pst:826 [in SpecCT]
pst:828 [in SpecCT]
pst:832 [in SpecCT]
pst:836 [in SpecCT]
pst:840 [in SpecCT]
pst:843 [in SpecCT]
pst:845 [in SpecCT]
pst:848 [in SpecCT]
pst:852 [in SpecCT]
pst:856 [in SpecCT]
pst:858 [in SpecCT]
ps:139 [in Noninterference]
ps:161 [in Noninterference]
pub:100 [in Noninterference]
pub:103 [in Noninterference]
pub:108 [in Noninterference]
pub:109 [in Noninterference]
pub:112 [in Noninterference]
pub:114 [in Noninterference]
pub:117 [in Noninterference]
pub:119 [in Noninterference]
pub:129 [in Noninterference]
pub:135 [in Noninterference]
pub:142 [in Noninterference]
pub:152 [in Noninterference]
pub:154 [in Noninterference]
pub:156 [in Noninterference]
pub:159 [in Noninterference]
pub:162 [in Noninterference]
pub:167 [in Noninterference]
pub:175 [in Noninterference]
pub:177 [in Noninterference]
pub:181 [in Noninterference]
pub:75 [in Noninterference]
pub:79 [in Noninterference]
pub:84 [in Noninterference]
pub:89 [in Noninterference]
pub:91 [in Noninterference]
pub:96 [in Noninterference]
P':64 [in RelHoare]
P':74 [in RelHoare]
P:1 [in RelHoare]
P:1 [in StaticIFC]
P:10 [in StaticIFC]
P:104 [in RelHoare]
P:111 [in RelHoare]
P:115 [in RelHoare]
P:119 [in RelHoare]
P:120 [in SpecCT]
P:123 [in RelHoare]
P:123 [in StaticIFC]
P:126 [in SpecCT]
P:127 [in RelHoare]
P:129 [in SpecCT]
P:133 [in SpecCT]
P:133 [in RelHoare]
P:136 [in StaticIFC]
P:137 [in SpecCT]
P:139 [in RelHoare]
P:14 [in StaticIFC]
P:140 [in StaticIFC]
P:142 [in StaticIFC]
P:144 [in StaticIFC]
P:146 [in StaticIFC]
P:150 [in SpecCT]
P:158 [in SpecCT]
P:159 [in RelHoare]
P:166 [in StaticIFC]
P:171 [in RelHoare]
P:171 [in StaticIFC]
P:174 [in StaticIFC]
P:177 [in RelHoare]
P:177 [in StaticIFC]
P:18 [in StaticIFC]
P:181 [in StaticIFC]
P:183 [in RelHoare]
P:185 [in StaticIFC]
P:189 [in RelHoare]
P:192 [in StaticIFC]
P:194 [in StaticIFC]
P:195 [in RelHoare]
P:200 [in StaticIFC]
P:201 [in RelHoare]
P:205 [in SpecCT]
P:207 [in RelHoare]
P:212 [in SpecCT]
P:212 [in RelHoare]
P:215 [in RelHoare]
P:216 [in SpecCT]
P:218 [in StaticIFC]
P:220 [in SpecCT]
P:221 [in StaticIFC]
P:223 [in StaticIFC]
P:227 [in StaticIFC]
P:233 [in StaticIFC]
P:241 [in SpecCT]
P:254 [in SpecCT]
P:269 [in StaticIFC]
P:277 [in StaticIFC]
P:33 [in StaticIFC]
P:353 [in SpecCT]
P:369 [in SpecCT]
P:414 [in SpecCT]
P:427 [in SpecCT]
P:431 [in SpecCT]
P:5 [in RelHoare]
P:50 [in StaticIFC]
P:522 [in SpecCT]
P:533 [in SpecCT]
P:54 [in RelHoare]
P:54 [in StaticIFC]
P:543 [in SpecCT]
P:554 [in SpecCT]
P:56 [in StaticIFC]
P:563 [in SpecCT]
P:59 [in StaticIFC]
P:611 [in SpecCT]
P:618 [in SpecCT]
P:62 [in RelHoare]
P:625 [in SpecCT]
P:63 [in RelHoare]
P:63 [in StaticIFC]
P:643 [in SpecCT]
P:660 [in SpecCT]
P:68 [in RelHoare]
P:680 [in SpecCT]
P:7 [in StaticIFC]
P:714 [in SpecCT]
P:728 [in SpecCT]
P:73 [in RelHoare]
P:751 [in SpecCT]
P:763 [in SpecCT]
P:775 [in SpecCT]
P:789 [in SpecCT]
P:799 [in SpecCT]
P:81 [in RelHoare]
P:86 [in RelHoare]
P:88 [in StaticIFC]
P:919 [in SpecCT]
P:92 [in StaticIFC]
P:94 [in StaticIFC]
P:97 [in StaticIFC]
Q
Q':70 [in RelHoare]Q':76 [in RelHoare]
Q:105 [in RelHoare]
Q:112 [in RelHoare]
Q:116 [in RelHoare]
Q:120 [in RelHoare]
Q:124 [in RelHoare]
Q:128 [in RelHoare]
Q:134 [in RelHoare]
Q:140 [in RelHoare]
Q:160 [in RelHoare]
Q:172 [in RelHoare]
Q:178 [in RelHoare]
Q:184 [in RelHoare]
Q:190 [in RelHoare]
Q:196 [in RelHoare]
Q:2 [in RelHoare]
Q:202 [in RelHoare]
Q:57 [in RelHoare]
Q:65 [in RelHoare]
Q:69 [in RelHoare]
Q:75 [in RelHoare]
Q:89 [in RelHoare]
Q:94 [in RelHoare]
Q:97 [in RelHoare]
R
R:106 [in RelHoare]R:129 [in RelHoare]
R:135 [in RelHoare]
R:141 [in Noninterference]
R:166 [in Noninterference]
S
sf:31 [in Noninterference]si1:14 [in Noninterference]
si1:23 [in Noninterference]
si2:15 [in Noninterference]
si2:24 [in Noninterference]
SI:17 [in Noninterference]
si:2 [in Noninterference]
SI:26 [in Noninterference]
si:33 [in Noninterference]
SI:35 [in Noninterference]
SI:40 [in Noninterference]
si:48 [in Noninterference]
si:5 [in Noninterference]
si:50 [in Noninterference]
SI:52 [in Noninterference]
si:58 [in Noninterference]
SI:60 [in Noninterference]
SI:66 [in Noninterference]
si:7 [in Noninterference]
si:72 [in Noninterference]
si:74 [in Noninterference]
SI:9 [in Noninterference]
some_si:69 [in Noninterference]
some_si:63 [in Noninterference]
some_si:55 [in Noninterference]
some_si:43 [in Noninterference]
SO:11 [in Noninterference]
SO:19 [in Noninterference]
SO:28 [in Noninterference]
SO:37 [in Noninterference]
SO:42 [in Noninterference]
SO:54 [in Noninterference]
SO:62 [in Noninterference]
SO:68 [in Noninterference]
ss:140 [in Noninterference]
ss:160 [in Noninterference]
stt1:921 [in SpecCT]
stt1:929 [in SpecCT]
stt2:925 [in SpecCT]
stt2:933 [in SpecCT]
st'':246 [in StaticIFC]
st'':282 [in SpecCT]
st'':451 [in SpecCT]
st'':80 [in SpecCT]
st':103 [in SpecCT]
st':245 [in StaticIFC]
st':250 [in StaticIFC]
st':256 [in StaticIFC]
st':267 [in StaticIFC]
st':279 [in SpecCT]
st':292 [in SpecCT]
st':303 [in SpecCT]
st':316 [in SpecCT]
st':403 [in SpecCT]
st':411 [in SpecCT]
st':448 [in SpecCT]
st':461 [in SpecCT]
st':472 [in SpecCT]
st':485 [in SpecCT]
st':732 [in SpecCT]
st':757 [in SpecCT]
st':769 [in SpecCT]
st':78 [in SpecCT]
st':781 [in SpecCT]
st':793 [in SpecCT]
st':86 [in SpecCT]
st':902 [in SpecCT]
st':915 [in SpecCT]
st':94 [in SpecCT]
st1':144 [in SpecCT]
st1':360 [in SpecCT]
st1':421 [in SpecCT]
st1':60 [in RelHoare]
st1':633 [in SpecCT]
st1':806 [in SpecCT]
st1:100 [in RelHoare]
st1:102 [in RelHoare]
st1:11 [in RelHoare]
st1:13 [in RelHoare]
st1:140 [in SpecCT]
st1:144 [in RelHoare]
st1:147 [in RelHoare]
st1:149 [in RelHoare]
st1:15 [in RelHoare]
st1:150 [in Noninterference]
st1:151 [in RelHoare]
st1:154 [in RelHoare]
st1:157 [in RelHoare]
st1:167 [in RelHoare]
st1:169 [in RelHoare]
st1:17 [in RelHoare]
st1:19 [in RelHoare]
st1:21 [in RelHoare]
st1:23 [in RelHoare]
st1:25 [in RelHoare]
st1:27 [in RelHoare]
st1:29 [in RelHoare]
st1:3 [in RelHoare]
st1:31 [in RelHoare]
st1:33 [in RelHoare]
st1:35 [in RelHoare]
st1:356 [in SpecCT]
st1:37 [in RelHoare]
st1:39 [in RelHoare]
st1:41 [in RelHoare]
st1:417 [in SpecCT]
st1:46 [in RelHoare]
st1:52 [in RelHoare]
st1:58 [in RelHoare]
st1:628 [in SpecCT]
st1:670 [in SpecCT]
st1:8 [in RelHoare]
st1:802 [in SpecCT]
st1:82 [in RelHoare]
st1:87 [in RelHoare]
st2':145 [in SpecCT]
st2':361 [in SpecCT]
st2':422 [in SpecCT]
st2':61 [in RelHoare]
st2':634 [in SpecCT]
st2':807 [in SpecCT]
st2:10 [in RelHoare]
st2:101 [in RelHoare]
st2:103 [in RelHoare]
st2:12 [in RelHoare]
st2:14 [in RelHoare]
st2:141 [in SpecCT]
st2:145 [in RelHoare]
st2:148 [in RelHoare]
st2:150 [in RelHoare]
st2:151 [in Noninterference]
st2:152 [in RelHoare]
st2:155 [in RelHoare]
st2:158 [in RelHoare]
st2:16 [in RelHoare]
st2:168 [in RelHoare]
st2:170 [in RelHoare]
st2:18 [in RelHoare]
st2:20 [in RelHoare]
st2:22 [in RelHoare]
st2:24 [in RelHoare]
st2:26 [in RelHoare]
st2:28 [in RelHoare]
st2:30 [in RelHoare]
st2:32 [in RelHoare]
st2:34 [in RelHoare]
st2:357 [in SpecCT]
st2:36 [in RelHoare]
st2:38 [in RelHoare]
st2:4 [in RelHoare]
st2:40 [in RelHoare]
st2:418 [in SpecCT]
st2:42 [in RelHoare]
st2:47 [in RelHoare]
st2:53 [in RelHoare]
st2:59 [in RelHoare]
st2:629 [in SpecCT]
st2:671 [in SpecCT]
st2:803 [in SpecCT]
st2:83 [in RelHoare]
st2:88 [in RelHoare]
st:101 [in SpecCT]
st:107 [in SpecCT]
st:113 [in SpecCT]
st:149 [in Noninterference]
st:237 [in StaticIFC]
st:238 [in StaticIFC]
st:244 [in StaticIFC]
st:249 [in StaticIFC]
st:255 [in StaticIFC]
st:262 [in StaticIFC]
st:265 [in SpecCT]
st:266 [in StaticIFC]
st:268 [in SpecCT]
st:276 [in SpecCT]
st:289 [in SpecCT]
st:300 [in SpecCT]
st:312 [in SpecCT]
st:321 [in SpecCT]
st:328 [in SpecCT]
st:336 [in SpecCT]
st:344 [in SpecCT]
st:401 [in SpecCT]
st:409 [in SpecCT]
st:434 [in SpecCT]
st:437 [in SpecCT]
st:44 [in SpecCT]
st:445 [in SpecCT]
st:458 [in SpecCT]
st:46 [in SpecCT]
st:469 [in SpecCT]
st:481 [in SpecCT]
st:490 [in SpecCT]
st:497 [in SpecCT]
st:505 [in SpecCT]
st:513 [in SpecCT]
st:67 [in SpecCT]
st:69 [in SpecCT]
st:729 [in SpecCT]
st:739 [in SpecCT]
st:744 [in SpecCT]
st:748 [in SpecCT]
st:752 [in SpecCT]
st:76 [in SpecCT]
st:764 [in SpecCT]
st:776 [in SpecCT]
st:790 [in SpecCT]
st:84 [in SpecCT]
st:887 [in SpecCT]
st:897 [in SpecCT]
st:911 [in SpecCT]
st:92 [in SpecCT]
s':138 [in Noninterference]
s':165 [in Noninterference]
s':180 [in Noninterference]
s':184 [in Noninterference]
s':184 [in StaticIFC]
s':226 [in StaticIFC]
s':376 [in SpecCT]
s':385 [in SpecCT]
s':394 [in SpecCT]
s':528 [in SpecCT]
s':539 [in SpecCT]
s':549 [in SpecCT]
s':558 [in SpecCT]
s':567 [in SpecCT]
s1':133 [in Noninterference]
s1':146 [in Noninterference]
s1':171 [in Noninterference]
s1':190 [in StaticIFC]
s1':198 [in StaticIFC]
s1':22 [in StaticIFC]
s1':231 [in StaticIFC]
s1':248 [in SpecCT]
s1':273 [in StaticIFC]
s1':651 [in SpecCT]
s1':688 [in SpecCT]
s1:101 [in Noninterference]
s1:11 [in StaticIFC]
s1:122 [in SpecCT]
s1:130 [in SpecCT]
s1:131 [in Noninterference]
s1:134 [in SpecCT]
s1:144 [in Noninterference]
s1:15 [in StaticIFC]
s1:157 [in Noninterference]
s1:169 [in Noninterference]
s1:188 [in StaticIFC]
s1:196 [in StaticIFC]
s1:20 [in StaticIFC]
s1:206 [in SpecCT]
s1:213 [in SpecCT]
s1:217 [in SpecCT]
s1:229 [in StaticIFC]
s1:244 [in SpecCT]
s1:271 [in StaticIFC]
s1:3 [in StaticIFC]
s1:60 [in StaticIFC]
s1:646 [in SpecCT]
s1:662 [in SpecCT]
s1:683 [in SpecCT]
s1:76 [in Noninterference]
s1:81 [in Noninterference]
s1:87 [in Noninterference]
s1:93 [in Noninterference]
s1:97 [in Noninterference]
s1:98 [in StaticIFC]
s2':134 [in Noninterference]
s2':147 [in Noninterference]
s2':172 [in Noninterference]
s2':191 [in StaticIFC]
s2':199 [in StaticIFC]
s2':23 [in StaticIFC]
s2':232 [in StaticIFC]
s2':249 [in SpecCT]
s2':274 [in StaticIFC]
s2':652 [in SpecCT]
s2':689 [in SpecCT]
s2:102 [in Noninterference]
s2:12 [in StaticIFC]
s2:123 [in SpecCT]
s2:131 [in SpecCT]
s2:132 [in Noninterference]
s2:135 [in SpecCT]
s2:145 [in Noninterference]
s2:158 [in Noninterference]
s2:16 [in StaticIFC]
s2:170 [in Noninterference]
s2:189 [in StaticIFC]
s2:197 [in StaticIFC]
s2:207 [in SpecCT]
s2:21 [in StaticIFC]
s2:214 [in SpecCT]
s2:218 [in SpecCT]
s2:230 [in StaticIFC]
s2:245 [in SpecCT]
s2:272 [in StaticIFC]
s2:4 [in StaticIFC]
s2:61 [in StaticIFC]
s2:647 [in SpecCT]
s2:663 [in SpecCT]
s2:684 [in SpecCT]
s2:77 [in Noninterference]
s2:82 [in Noninterference]
s2:88 [in Noninterference]
s2:94 [in Noninterference]
s2:98 [in Noninterference]
s2:99 [in StaticIFC]
s3:136 [in SpecCT]
s3:17 [in StaticIFC]
s:104 [in Noninterference]
s:107 [in Noninterference]
s:113 [in Noninterference]
s:118 [in Noninterference]
s:121 [in Noninterference]
s:127 [in SpecCT]
s:128 [in Noninterference]
s:137 [in Noninterference]
s:155 [in Noninterference]
s:164 [in Noninterference]
s:179 [in Noninterference]
s:183 [in Noninterference]
s:183 [in StaticIFC]
s:225 [in StaticIFC]
s:372 [in SpecCT]
s:381 [in SpecCT]
s:390 [in SpecCT]
s:524 [in SpecCT]
s:535 [in SpecCT]
s:545 [in SpecCT]
s:556 [in SpecCT]
s:565 [in SpecCT]
s:8 [in StaticIFC]
s:83 [in Noninterference]
T
t1:163 [in RelHoare]t1:174 [in RelHoare]
t1:186 [in RelHoare]
t1:192 [in RelHoare]
t1:581 [in SpecCT]
t1:586 [in SpecCT]
t1:613 [in SpecCT]
t1:620 [in SpecCT]
t2:164 [in RelHoare]
t2:181 [in RelHoare]
t2:199 [in RelHoare]
t2:205 [in RelHoare]
t2:582 [in SpecCT]
t2:587 [in SpecCT]
t2:614 [in SpecCT]
t2:621 [in SpecCT]
U
u:907 [in SpecCT]V
value:820 [in SpecCT]value:831 [in SpecCT]
value:839 [in SpecCT]
v:850 [in SpecCT]
v:854 [in SpecCT]
v:866 [in SpecCT]
X
xs:571 [in SpecCT]xs:591 [in SpecCT]
X1:90 [in RelHoare]
X2:91 [in RelHoare]
x:109 [in SpecCT]
X:121 [in SpecCT]
x:122 [in Noninterference]
x:123 [in Noninterference]
x:124 [in SpecCT]
x:124 [in Noninterference]
X:125 [in SpecCT]
x:125 [in Noninterference]
x:126 [in Noninterference]
X:126 [in StaticIFC]
X:128 [in SpecCT]
X:13 [in StaticIFC]
X:132 [in SpecCT]
X:151 [in StaticIFC]
X:164 [in SpecCT]
x:173 [in Noninterference]
x:174 [in Noninterference]
X:2 [in StaticIFC]
X:205 [in StaticIFC]
X:224 [in SpecCT]
x:234 [in SpecCT]
x:241 [in StaticIFC]
x:273 [in SpecCT]
x:29 [in SpecCT]
x:324 [in SpecCT]
x:330 [in SpecCT]
X:37 [in StaticIFC]
x:38 [in SpecCT]
X:43 [in RelHoare]
x:442 [in SpecCT]
x:45 [in RelHoare]
X:48 [in RelHoare]
x:493 [in SpecCT]
x:499 [in SpecCT]
x:5 [in StaticIFC]
x:50 [in RelHoare]
X:570 [in SpecCT]
X:574 [in SpecCT]
X:576 [in SpecCT]
X:578 [in SpecCT]
X:583 [in SpecCT]
X:588 [in SpecCT]
x:589 [in SpecCT]
X:593 [in SpecCT]
X:597 [in SpecCT]
x:6 [in SpecCT]
X:6 [in StaticIFC]
X:602 [in SpecCT]
X:606 [in SpecCT]
X:615 [in SpecCT]
X:622 [in SpecCT]
x:697 [in SpecCT]
x:699 [in SpecCT]
x:705 [in SpecCT]
x:73 [in SpecCT]
X:738 [in SpecCT]
X:743 [in SpecCT]
X:747 [in SpecCT]
X:761 [in SpecCT]
X:773 [in SpecCT]
x:78 [in Noninterference]
X:785 [in SpecCT]
X:79 [in RelHoare]
X:84 [in RelHoare]
x:86 [in Noninterference]
X:9 [in StaticIFC]
x:90 [in Noninterference]
X:95 [in RelHoare]
X:98 [in RelHoare]
x:99 [in Noninterference]
Y
ys:572 [in SpecCT]ys:592 [in SpecCT]
y:51 [in RelHoare]
y:590 [in SpecCT]
Z
zs:573 [in SpecCT]z1:105 [in Noninterference]
z2:106 [in Noninterference]
Module Index
S
SpecCTInterpreter [in SpecCT]Library Index
N
NoninterferenceR
RelHoareS
SpecCTStaticIFC
Lemma Index
A
add42_monotonic [in RelHoare]aeval_unused_update [in SpecCT]
aeval_beval_unused_update [in SpecCT]
app_eq_prefix [in SpecCT]
aux [in SpecCT]
B
beval_unused_update [in SpecCT]bexp_eval_false_2 [in RelHoare]
bexp_eval_false_1 [in RelHoare]
broken_def_accepts_insecure_f [in Noninterference]
broken_def_rejects_secure_f [in Noninterference]
C
cannot_flow_secret_public [in StaticIFC]can_flow_join_r2 [in StaticIFC]
can_flow_join_r1 [in StaticIFC]
can_flow_join_l [in StaticIFC]
can_flow_join_2 [in StaticIFC]
can_flow_join_1 [in StaticIFC]
can_flow_trans [in StaticIFC]
can_flow_refl [in StaticIFC]
can_flow_secret [in StaticIFC]
can_flow_public [in StaticIFC]
constant_sme_insecure_f [in Noninterference]
cteval_equiv_seq_spec_eval [in SpecCT]
ct_well_typed_ideal_noninterferent [in SpecCT]
ct_well_typed_ideal_noninterferent_general [in SpecCT]
ct_well_typed_seq_spec_eval_ct_secure [in SpecCT]
ct_well_typed_ct_secure [in SpecCT]
ct_well_typed_noninterferent [in SpecCT]
D
dead_store_example [in RelHoare]different_code [in StaticIFC]
I
ideal_unused_update_rev [in SpecCT]ideal_unused_update [in SpecCT]
ideal_unused_overwrite [in SpecCT]
ideal_spec_ct_secure [in SpecCT]
interferent_secore_com2 [in Noninterference]
interferent_secore_com1 [in Noninterference]
interferent_insecure_f [in Noninterference]
J
join_public [in SpecCT]join_secret_l [in StaticIFC]
join_public_r [in StaticIFC]
join_public_l [in StaticIFC]
join_public [in StaticIFC]
join_commutative [in StaticIFC]
L
label_of_bexp_unique [in StaticIFC]label_of_bexp_sound [in StaticIFC]
label_of_aexp_unique [in StaticIFC]
label_of_aexp_sound [in StaticIFC]
M
merge_state_pub_equiv [in Noninterference]merge_states_split_state [in Noninterference]
N
noninterferent_bexp [in SpecCT]noninterferent_aexp [in SpecCT]
noninterferent_aexp_bexp [in SpecCT]
noninterferent_while_sme [in Noninterference]
noninterferent_secore_com' [in Noninterference]
noninterferent_sme_insecure_com2 [in Noninterference]
noninterferent_sme_insecure_com1 [in Noninterference]
noninterferent_secore_com [in Noninterference]
noninterferent_sme_state [in Noninterference]
noninterferent_state_ni [in Noninterference]
noninterferent_sme [in Noninterference]
noninterferent_splittable [in Noninterference]
noninterferent_secure_f [in Noninterference]
noninterferent_bexp [in StaticIFC]
noninterferent_aexp [in StaticIFC]
P
pceval_ceval [in StaticIFC]pc_well_typed_pc_secure [in StaticIFC]
pc_well_typed_noninterferent [in StaticIFC]
pc_typechecker_complete [in StaticIFC]
pc_typechecker_sound [in StaticIFC]
prefix_append_front [in SpecCT]
prefix_app [in SpecCT]
prefix_cons [in SpecCT]
prefix_or_heads [in SpecCT]
prefix_heads [in SpecCT]
prefix_heads_and_tails [in SpecCT]
prefix_nil [in SpecCT]
prefix_refl [in SpecCT]
prog_size_monotonic [in SpecCT]
pub_equiv_update_secret [in SpecCT]
pub_equiv_update_public [in SpecCT]
pub_equiv_trans [in SpecCT]
pub_equiv_sym [in SpecCT]
pub_equiv_refl [in SpecCT]
pub_equiv_sym [in Noninterference]
pub_equiv_split_state [in Noninterference]
pub_equiv_merge_states [in Noninterference]
pub_equiv_split_iff [in Noninterference]
pub_equiv_trans [in StaticIFC]
pub_equiv_sym [in StaticIFC]
pub_equiv_refl [in StaticIFC]
R
rhoare_while_2 [in RelHoare]rhoare_while_1 [in RelHoare]
rhoare_while [in RelHoare]
rhoare_if_false_2 [in RelHoare]
rhoare_if_true_2 [in RelHoare]
rhoare_if_false_1 [in RelHoare]
rhoare_if_true_1 [in RelHoare]
rhoare_if_2 [in RelHoare]
rhoare_if_1 [in RelHoare]
rhoare_if [in RelHoare]
rhoare_equiv_skip_l_1' [in RelHoare]
rhoare_seq_2 [in RelHoare]
rhoare_seq_1 [in RelHoare]
rhoare_seq_skip_2 [in RelHoare]
rhoare_skip_seq_2 [in RelHoare]
rhoare_seq_skip_1 [in RelHoare]
rhoare_skip_seq_1 [in RelHoare]
rhoare_seq [in RelHoare]
rhoare_asgn_2 [in RelHoare]
rhoare_asgn_1 [in RelHoare]
rhoare_asgn [in RelHoare]
rhoare_consequence [in RelHoare]
rhoare_consequence_post [in RelHoare]
rhoare_consequence_pre [in RelHoare]
rhoare_skip [in RelHoare]
S
secret_run [in StaticIFC]secure_com_noninterferent [in RelHoare]
secure_f_rejected_again [in Noninterference]
sel_slh_spec_ct_secure [in SpecCT]
sel_slh_ideal [in SpecCT]
sel_slh_flag [in SpecCT]
seq_spec_eval_ideal_eval [in SpecCT]
seq_eval_ideal_eval_ind2 [in SpecCT]
seq_eval_ideal_eval_ind1 [in SpecCT]
somewhat_transparent_while_sme [in Noninterference]
SpecCTInterpreter.eqb_reflect [in SpecCT]
SpecCTInterpreter.ltb_reflect [in SpecCT]
SpecCTInterpreter.spec_eval_engine_sound [in SpecCT]
SpecCTInterpreter.spec_eval_engine_aux_sound [in SpecCT]
speculation_needs_force_ideal [in SpecCT]
speculation_needs_force [in SpecCT]
speculation_bit_monotonic [in SpecCT]
splittable_noninterferent [in Noninterference]
T
terminating_noninterferent_tsni [in Noninterference]transparent_sme_state [in Noninterference]
transparent_sme [in Noninterference]
trivial_assignment_skip' [in RelHoare]
trivial_assignment_skip [in RelHoare]
tsni_transparent_while_sme [in Noninterference]
tsni_noninterferent [in Noninterference]
ts_well_typed_tsni [in StaticIFC]
ts_well_typed_equitermination [in StaticIFC]
ts_secret_run_terminating [in StaticIFC]
ts_well_typed_noninterferent [in StaticIFC]
ts_well_typed_well_typed [in StaticIFC]
U
unsafe_access_needs_speculation [in SpecCT]W
weaken_pc [in StaticIFC]well_typed_noninterferent [in StaticIFC]
wt_typechecker_complete [in StaticIFC]
wt_typechecker_sound [in StaticIFC]
X
xpubX [in Noninterference]xpub_true [in Noninterference]
Y
Y_neq_X [in Noninterference]Constructor Index
A
ACTIf [in SpecCT]AId [in SpecCT]
AMinus [in SpecCT]
AMult [in SpecCT]
ANum [in SpecCT]
APlus [in SpecCT]
ARead [in SpecCT]
Asgn [in SpecCT]
AWrite [in SpecCT]
B
BAnd [in SpecCT]BEq [in SpecCT]
BFalse [in SpecCT]
BGt [in SpecCT]
BLe [in SpecCT]
BNeq [in SpecCT]
BNot [in SpecCT]
BTrue [in SpecCT]
C
CTE_Write [in SpecCT]CTE_ARead [in SpecCT]
CTE_While [in SpecCT]
CTE_IfFalse [in SpecCT]
CTE_IfTrue [in SpecCT]
CTE_Seq [in SpecCT]
CTE_Asgn [in SpecCT]
CTE_Skip [in SpecCT]
CT_AWrite [in SpecCT]
CT_ARead [in SpecCT]
CT_While [in SpecCT]
CT_If [in SpecCT]
CT_Seq [in SpecCT]
CT_Asgn [in SpecCT]
CT_Skip [in SpecCT]
D
DForce [in SpecCT]DLoad [in SpecCT]
DStep [in SpecCT]
DStore [in SpecCT]
E
E_While [in StaticIFC]E_IfFalse [in StaticIFC]
E_IfTrue [in StaticIFC]
E_Seq [in StaticIFC]
E_Asgn [in StaticIFC]
E_Skip [in StaticIFC]
I
Ideal_Write_U [in SpecCT]Ideal_Write [in SpecCT]
Ideal_ARead_U [in SpecCT]
Ideal_ARead [in SpecCT]
Ideal_While [in SpecCT]
Ideal_If_F [in SpecCT]
Ideal_If [in SpecCT]
Ideal_Seq [in SpecCT]
Ideal_Asgn [in SpecCT]
Ideal_Skip [in SpecCT]
If [in SpecCT]
O
OARead [in SpecCT]OAWrite [in SpecCT]
OBranch [in SpecCT]
P
PCWT_While [in StaticIFC]PCWT_If [in StaticIFC]
PCWT_Seq [in StaticIFC]
PCWT_Asgn [in StaticIFC]
PCWT_Com [in StaticIFC]
S
Seq [in SpecCT]Skip [in SpecCT]
SpecCTInterpreter.OST_Finished [in SpecCT]
SpecCTInterpreter.OST_OutOfFuel [in SpecCT]
SpecCTInterpreter.OST_Error [in SpecCT]
Spec_Write_U [in SpecCT]
Spec_Write [in SpecCT]
Spec_ARead_U [in SpecCT]
Spec_ARead [in SpecCT]
Spec_While [in SpecCT]
Spec_If_F [in SpecCT]
Spec_If [in SpecCT]
Spec_Seq [in SpecCT]
Spec_Asgn [in SpecCT]
Spec_Skip [in SpecCT]
T
TS_While [in StaticIFC]TS_If [in StaticIFC]
TS_Seq [in StaticIFC]
TS_Asgn [in StaticIFC]
TS_Com [in StaticIFC]
T_And [in SpecCT]
T_Not [in SpecCT]
T_Gt [in SpecCT]
T_Le [in SpecCT]
T_Neq [in SpecCT]
T_Eq [in SpecCT]
T_False [in SpecCT]
T_True [in SpecCT]
T_CTIf [in SpecCT]
T_Mult [in SpecCT]
T_Minus [in SpecCT]
T_Plus [in SpecCT]
T_Id [in SpecCT]
T_Num [in SpecCT]
T_And [in StaticIFC]
T_Not [in StaticIFC]
T_Gt [in StaticIFC]
T_Le [in StaticIFC]
T_Neq [in StaticIFC]
T_Eq [in StaticIFC]
T_False [in StaticIFC]
T_True [in StaticIFC]
T_Mult [in StaticIFC]
T_Minus [in StaticIFC]
T_Plus [in StaticIFC]
T_Id [in StaticIFC]
T_Num [in StaticIFC]
W
While [in SpecCT]WT_While [in StaticIFC]
WT_If [in StaticIFC]
WT_Seq [in StaticIFC]
WT_Asgn [in StaticIFC]
WT_Com [in StaticIFC]
Axiom Index
P
prog_size_ind [in SpecCT]Inductive Index
A
aexp [in SpecCT]aexp_has_label [in SpecCT]
aexp_has_label [in StaticIFC]
B
bexp [in SpecCT]bexp_has_label [in SpecCT]
bexp_has_label [in StaticIFC]
C
com [in SpecCT]cteval [in SpecCT]
ct_well_typed [in SpecCT]
D
direction [in SpecCT]I
ideal_eval [in SpecCT]O
observation [in SpecCT]P
pceval [in StaticIFC]pc_well_typed [in StaticIFC]
S
SpecCTInterpreter.output_st [in SpecCT]spec_eval [in SpecCT]
T
ts_well_typed [in StaticIFC]W
well_typed [in StaticIFC]Abbreviation Index
M
mkAexp [in RelHoare]R
rassert [in RelHoare]Definition Index
A
A [in SpecCT]add42_monotonic_spec [in RelHoare]
aeval [in SpecCT]
Aexp [in RelHoare]
aexp_bexp_has_label_mutind [in SpecCT]
aexp_bexp_has_label_ind [in SpecCT]
aexp_bexp_mutind [in SpecCT]
aexp_bexp_ind [in SpecCT]
Aexp_of_aexp_2 [in RelHoare]
Aexp_of_aexp_1 [in RelHoare]
Aexp_of_nat [in RelHoare]
AP [in SpecCT]
ap [in RelHoare]
ap2 [in RelHoare]
AS [in SpecCT]
assn_sub_2 [in RelHoare]
assn_sub_1 [in RelHoare]
astate [in SpecCT]
a_unused [in SpecCT]
B
bassn_2 [in RelHoare]bassn_1 [in RelHoare]
beval [in SpecCT]
bexp_aexp_has_label_ind [in SpecCT]
bexp_aexp_ind [in SpecCT]
branches [in StaticIFC]
broken_def [in Noninterference]
b_unused [in SpecCT]
C
can_flow [in SpecCT]can_flow [in StaticIFC]
com_size [in SpecCT]
ct_insecure_prog_is_not_ct_secure [in SpecCT]
ct_insecure_prog [in SpecCT]
ct_secure [in SpecCT]
D
dirs [in SpecCT]E
example1_sme_insecure_f [in Noninterference]example1_secure_f [in Noninterference]
example2_sme_insecure_f [in Noninterference]
example2_secure_f [in Noninterference]
example3_sme_insecure_f [in Noninterference]
example3_secure_f [in Noninterference]
F
fact_iter_slow [in RelHoare]fact_iter_fast [in RelHoare]
FILL_IN_HERE [in RelHoare]
FILL_IN_HERE [in StaticIFC]
I
insecure_com2 [in Noninterference]insecure_com1 [in Noninterference]
insecure_f [in Noninterference]
insecure_com2 [in StaticIFC]
insecure_com1 [in StaticIFC]
interferent_insecure_com1 [in StaticIFC]
J
join [in SpecCT]join [in StaticIFC]
L
label [in SpecCT]label [in StaticIFC]
label_of_bexp [in StaticIFC]
label_of_aexp [in StaticIFC]
M
merge_states [in Noninterference]N
noninterference_crossproduct [in RelHoare]noninterference_lockstep [in RelHoare]
noninterferent [in Noninterference]
noninterferent [in StaticIFC]
noninterferent_while_R [in Noninterference]
noninterferent_while [in Noninterference]
noninterferent_no_while [in Noninterference]
noninterferent_state [in Noninterference]
noninterferent_secure_com [in StaticIFC]
not_wt_insecure_com2 [in StaticIFC]
not_swt_noninterferent_com_is_noninterferent [in StaticIFC]
not_swt_noninterferent_com [in StaticIFC]
not_swt_insecure_com2 [in StaticIFC]
not_swt_insecure_com1 [in StaticIFC]
O
obs [in SpecCT]P
pc_secure [in StaticIFC]pc_typechecker [in StaticIFC]
prefix [in SpecCT]
prog_size [in SpecCT]
public [in SpecCT]
public [in StaticIFC]
pub_equiv [in SpecCT]
pub_arrs [in SpecCT]
pub_vars [in SpecCT]
pub_equiv_split [in Noninterference]
pub_equiv [in Noninterference]
pub_map [in Noninterference]
pub_equiv [in StaticIFC]
pub_vars [in StaticIFC]
p1 [in RelHoare]
p2 [in RelHoare]
R
RAssertion [in RelHoare]rassert_of_Prop [in RelHoare]
rassert_implies [in RelHoare]
rhoare_judgment [in RelHoare]
S
secret [in SpecCT]secret [in StaticIFC]
secure_com_noninterferent_spec [in RelHoare]
secure_com [in RelHoare]
secure_com [in Noninterference]
secure_f [in Noninterference]
secure_p2 [in StaticIFC]
secure_com1' [in StaticIFC]
secure_com [in StaticIFC]
sel_slh_ideal_prop [in SpecCT]
sel_slh_flag_prop [in SpecCT]
sel_slh [in SpecCT]
seq_ideal_eval [in SpecCT]
seq_spec_eval [in SpecCT]
sme [in Noninterference]
sme_while [in Noninterference]
sme_insecure_com2 [in Noninterference]
sme_insecure_com1 [in Noninterference]
sme_cmd [in Noninterference]
sme_state [in Noninterference]
SpecCTInterpreter.bind [in SpecCT]
SpecCTInterpreter.compute_fuel [in SpecCT]
SpecCTInterpreter.evaluator [in SpecCT]
SpecCTInterpreter.eval_bexp [in SpecCT]
SpecCTInterpreter.eval_aexp [in SpecCT]
SpecCTInterpreter.fetch_direction [in SpecCT]
SpecCTInterpreter.finish [in SpecCT]
SpecCTInterpreter.get_arr [in SpecCT]
SpecCTInterpreter.get_var [in SpecCT]
SpecCTInterpreter.interpreter [in SpecCT]
SpecCTInterpreter.is_speculating [in SpecCT]
SpecCTInterpreter.observe [in SpecCT]
SpecCTInterpreter.prog_st [in SpecCT]
SpecCTInterpreter.raise_error [in SpecCT]
SpecCTInterpreter.ret [in SpecCT]
SpecCTInterpreter.set_arr [in SpecCT]
SpecCTInterpreter.set_var [in SpecCT]
SpecCTInterpreter.spec_insecure_prog_2_is_ct_and_spec_insecure [in SpecCT]
SpecCTInterpreter.spec_insecure_prog_2 [in SpecCT]
SpecCTInterpreter.spec_eval_engine [in SpecCT]
SpecCTInterpreter.spec_eval_engine_aux [in SpecCT]
SpecCTInterpreter.start_speculating [in SpecCT]
spec_insecure_prog_is_ct_and_spec_insecure [in SpecCT]
spec_insecure_prog [in SpecCT]
spec_ct_secure [in SpecCT]
splittable [in Noninterference]
split_state_fun [in Noninterference]
split_state [in Noninterference]
state [in SpecCT]
swap_equiv_spec [in RelHoare]
swap_aux' [in RelHoare]
swap_arith [in RelHoare]
swap_aux [in RelHoare]
swt_secure_com [in StaticIFC]
T
termination_leak [in Noninterference]tini_secure_termination_leak [in Noninterference]
too_strong_def [in Noninterference]
trivial_skip [in RelHoare]
tsni [in StaticIFC]
tsni_insecure_termination_leak [in Noninterference]
tsni_while_R [in Noninterference]
U
unused [in SpecCT]upd [in SpecCT]
W
W [in SpecCT]wt_noninterferent_com [in StaticIFC]
wt_typechecker [in StaticIFC]
X
X [in SpecCT]xpub [in Noninterference]
xpub [in StaticIFC]
Y
Y [in SpecCT]Z
Z [in SpecCT]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2056 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (66 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1535 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (152 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (114 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (163 entries) |
This page has been generated by coqdoc