| 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 | (566 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) |
| 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 | (151 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 | (209 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_ind [definition, in SpecCT]
aexp_has_label_sind [definition, in SpecCT]
aexp_has_label_ind [definition, in SpecCT]
aexp_has_label [inductive, in SpecCT]
aexp_bexp_ind [definition, in SpecCT]
aexp_sind [definition, in SpecCT]
aexp_rec [definition, in SpecCT]
aexp_ind [definition, in SpecCT]
aexp_rect [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_sind [definition, in StaticIFC]
aexp_has_label_ind [definition, in StaticIFC]
aexp_has_label [inductive, in StaticIFC]
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]
AS [definition, in SpecCT]
Asgn [constructor, in SpecCT]
assn_sub_2 [definition, in RelHoare]
assn_sub_1 [definition, in RelHoare]
astate [definition, in SpecCT]
aux [lemma, in SpecCT]
AWrite [constructor, in SpecCT]
a_unused [definition, in SpecCT]
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_sind [definition, in SpecCT]
bexp_has_label_ind [definition, in SpecCT]
bexp_has_label [inductive, in SpecCT]
bexp_aexp_ind [definition, in SpecCT]
bexp_sind [definition, in SpecCT]
bexp_rec [definition, in SpecCT]
bexp_ind [definition, in SpecCT]
bexp_rect [definition, in SpecCT]
bexp_eval_false_2 [lemma, in RelHoare]
bexp_eval_false_1 [lemma, in RelHoare]
bexp_has_label_sind [definition, in StaticIFC]
bexp_has_label_ind [definition, in StaticIFC]
bexp_has_label [inductive, in StaticIFC]
BFalse [constructor, in SpecCT]
BGt [constructor, in SpecCT]
BLe [constructor, in SpecCT]
BNeq [constructor, in SpecCT]
BNot [constructor, 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]
BTrue [constructor, in SpecCT]
b_unused [definition, 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]
cinterp [definition, in Noninterference]
com [inductive, in SpecCT]
com_size [definition, in SpecCT]
com_sind [definition, in SpecCT]
com_rec [definition, in SpecCT]
com_ind [definition, in SpecCT]
com_rect [definition, in SpecCT]
constant_sme_insecure_f [lemma, in Noninterference]
cteval [inductive, in SpecCT]
cteval_equiv_seq_spec_eval [lemma, in SpecCT]
cteval_sind [definition, in SpecCT]
cteval_ind [definition, 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_well_typed_sind [definition, in SpecCT]
ct_well_typed_ind [definition, 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]
D
dead_store_example [lemma, in RelHoare]DForce [constructor, in SpecCT]
different_code [lemma, in StaticIFC]
direction [inductive, in SpecCT]
direction_sind [definition, in SpecCT]
direction_rec [definition, in SpecCT]
direction_ind [definition, in SpecCT]
direction_rect [definition, in SpecCT]
dirs [definition, in SpecCT]
DLoad [constructor, in SpecCT]
DStep [constructor, in SpecCT]
DStore [constructor, 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]
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]
flip [definition, in Noninterference]
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_eval_sind [definition, in SpecCT]
ideal_eval_ind [definition, 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]
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_insecure_com2 [lemma, in Noninterference]
interferent_insecure_com1 [lemma, in Noninterference]
interferent_insecure_f [lemma, in Noninterference]
interferent_insecure_com1 [definition, in StaticIFC]
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]
M
merge_state_pub_equiv [lemma, in Noninterference]merge_states_split_state [lemma, in Noninterference]
merge_states [definition, in Noninterference]
mkAexp [abbreviation, in RelHoare]
N
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_secure_com' [lemma, in Noninterference]
noninterferent_while [definition, in Noninterference]
noninterferent_sme_cmd [lemma, in Noninterference]
noninterferent_secure_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]
O
OARead [constructor, in SpecCT]OAWrite [constructor, in SpecCT]
OBranch [constructor, in SpecCT]
obs [definition, in SpecCT]
observation [inductive, in SpecCT]
observation_sind [definition, in SpecCT]
observation_rec [definition, in SpecCT]
observation_ind [definition, in SpecCT]
observation_rect [definition, in SpecCT]
P
pceval [inductive, in StaticIFC]pceval_ceval [lemma, in StaticIFC]
pceval_sind [definition, in StaticIFC]
pceval_ind [definition, 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_sind [definition, in StaticIFC]
pc_well_typed_ind [definition, in StaticIFC]
pc_well_typed [inductive, in StaticIFC]
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]
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]
p1 [definition, in RelHoare]
p2 [definition, 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]
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]
Skip [constructor, in SpecCT]
sme [definition, in Noninterference]
sme_while [definition, in Noninterference]
sme_cmd [definition, in Noninterference]
sme_state [definition, in Noninterference]
somewhat_transparent_while_sme [lemma, 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_sind [definition, in SpecCT]
SpecCTInterpreter.output_st_rec [definition, in SpecCT]
SpecCTInterpreter.output_st_ind [definition, in SpecCT]
SpecCTInterpreter.output_st_rect [definition, 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_eval_sind [definition, in SpecCT]
spec_eval_ind [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]
state [definition, in SpecCT]
StaticIFC [library]
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]
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_well_typed_sind [definition, in StaticIFC]
ts_well_typed_ind [definition, 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]
U
unsafe_access_needs_speculation [lemma, in SpecCT]unused [definition, in SpecCT]
upd [definition, in SpecCT]
W
W [definition, in SpecCT]weaken_pc [lemma, in StaticIFC]
well_typed_noninterferent [lemma, in StaticIFC]
well_typed_sind [definition, in StaticIFC]
well_typed_ind [definition, 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]
Y
Y [definition, in SpecCT]Y_neq_X [lemma, in Noninterference]
Z
Z [definition, in SpecCT]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]
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_insecure_com2 [in Noninterference]
interferent_insecure_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_secure_com' [in Noninterference]
noninterferent_sme_cmd [in Noninterference]
noninterferent_secure_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_ind [in SpecCT]
aexp_has_label_sind [in SpecCT]
aexp_has_label_ind [in SpecCT]
aexp_bexp_ind [in SpecCT]
aexp_sind [in SpecCT]
aexp_rec [in SpecCT]
aexp_ind [in SpecCT]
aexp_rect [in SpecCT]
Aexp_of_aexp_2 [in RelHoare]
Aexp_of_aexp_1 [in RelHoare]
Aexp_of_nat [in RelHoare]
aexp_has_label_sind [in StaticIFC]
aexp_has_label_ind [in StaticIFC]
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_has_label_sind [in SpecCT]
bexp_has_label_ind [in SpecCT]
bexp_aexp_ind [in SpecCT]
bexp_sind [in SpecCT]
bexp_rec [in SpecCT]
bexp_ind [in SpecCT]
bexp_rect [in SpecCT]
bexp_has_label_sind [in StaticIFC]
bexp_has_label_ind [in StaticIFC]
branches [in StaticIFC]
broken_def [in Noninterference]
b_unused [in SpecCT]
C
can_flow [in SpecCT]can_flow [in StaticIFC]
cinterp [in Noninterference]
com_size [in SpecCT]
com_sind [in SpecCT]
com_rec [in SpecCT]
com_ind [in SpecCT]
com_rect [in SpecCT]
cteval_sind [in SpecCT]
cteval_ind [in SpecCT]
ct_well_typed_sind [in SpecCT]
ct_well_typed_ind [in SpecCT]
ct_insecure_prog_is_not_ct_secure [in SpecCT]
ct_insecure_prog [in SpecCT]
ct_secure [in SpecCT]
D
direction_sind [in SpecCT]direction_rec [in SpecCT]
direction_ind [in SpecCT]
direction_rect [in SpecCT]
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]
flip [in Noninterference]
I
ideal_eval_sind [in SpecCT]ideal_eval_ind [in SpecCT]
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]observation_sind [in SpecCT]
observation_rec [in SpecCT]
observation_ind [in SpecCT]
observation_rect [in SpecCT]
P
pceval_sind [in StaticIFC]pceval_ind [in StaticIFC]
pc_secure [in StaticIFC]
pc_typechecker [in StaticIFC]
pc_well_typed_sind [in StaticIFC]
pc_well_typed_ind [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_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.output_st_sind [in SpecCT]
SpecCTInterpreter.output_st_rec [in SpecCT]
SpecCTInterpreter.output_st_ind [in SpecCT]
SpecCTInterpreter.output_st_rect [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]
spec_eval_sind [in SpecCT]
spec_eval_ind [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]
ts_well_typed_sind [in StaticIFC]
ts_well_typed_ind [in StaticIFC]
U
unused [in SpecCT]upd [in SpecCT]
W
W [in SpecCT]well_typed_sind [in StaticIFC]
well_typed_ind [in StaticIFC]
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 | (566 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) |
| 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 | (151 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 | (209 entries) |
This page has been generated by coqdoc