| 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 | (1417 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 | (1077 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 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 | (135 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 | (21 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 | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 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 | (127 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Global Index
A
about_generate_new_block [lemma, in Giskard.structures]about_non_last_block [axiom, in Giskard.structures]
about_generate_last_block [axiom, in Giskard.structures]
about_local_out_messages [lemma, in Giskard.local]
about_highest_message_in_list [lemma, in Giskard.local]
add [definition, in Giskard.local]
add_plural [definition, in Giskard.local]
at_least_second_highest [definition, in Giskard.precommit]
A:1 [binder, in Giskard.lib]
B
block [axiom, in Giskard.structures]block_eq_dec [definition, in Giskard.structures]
block_eqb_correct [axiom, in Giskard.structures]
block_eqb [axiom, in Giskard.structures]
broadcast_messages [definition, in Giskard.global]
b_child:5 [binder, in Giskard.commit]
b_child:166 [binder, in Giskard.precommit]
b_child:86 [binder, in Giskard.precommit]
b_child:79 [binder, in Giskard.precommit]
b_child:5 [binder, in Giskard.precommit]
b_last [definition, in Giskard.structures]
b_index [axiom, in Giskard.structures]
b_height [axiom, in Giskard.structures]
b':112 [binder, in Giskard.precommit]
b':143 [binder, in Giskard.precommit]
b1:10 [binder, in Giskard.commit]
b1:113 [binder, in Giskard.structures]
b1:12 [binder, in Giskard.structures]
b1:146 [binder, in Giskard.precommit]
b1:151 [binder, in Giskard.precommit]
b1:157 [binder, in Giskard.precommit]
b1:160 [binder, in Giskard.global]
b1:171 [binder, in Giskard.precommit]
b1:22 [binder, in Giskard.structures]
b1:253 [binder, in Giskard.global]
b1:384 [binder, in Giskard.precommit]
b1:390 [binder, in Giskard.precommit]
b1:396 [binder, in Giskard.precommit]
b1:5 [binder, in Giskard.prepare]
b1:50 [binder, in Giskard.prepare]
b1:64 [binder, in Giskard.prepare]
b1:73 [binder, in Giskard.precommit]
b1:76 [binder, in Giskard.prepare]
b1:9 [binder, in Giskard.structures]
b1:91 [binder, in Giskard.precommit]
b2:10 [binder, in Giskard.structures]
b2:11 [binder, in Giskard.commit]
b2:114 [binder, in Giskard.structures]
b2:13 [binder, in Giskard.structures]
b2:152 [binder, in Giskard.precommit]
b2:158 [binder, in Giskard.precommit]
b2:172 [binder, in Giskard.precommit]
b2:23 [binder, in Giskard.structures]
b2:385 [binder, in Giskard.precommit]
b2:391 [binder, in Giskard.precommit]
b2:397 [binder, in Giskard.precommit]
b2:51 [binder, in Giskard.prepare]
b2:6 [binder, in Giskard.prepare]
b2:74 [binder, in Giskard.precommit]
b2:92 [binder, in Giskard.precommit]
b:104 [binder, in Giskard.precommit]
b:105 [binder, in Giskard.precommit]
b:111 [binder, in Giskard.precommit]
b:116 [binder, in Giskard.precommit]
b:127 [binder, in Giskard.precommit]
b:129 [binder, in Giskard.precommit]
b:13 [binder, in Giskard.precommit]
b:135 [binder, in Giskard.precommit]
b:136 [binder, in Giskard.precommit]
b:142 [binder, in Giskard.precommit]
b:16 [binder, in Giskard.structures]
b:165 [binder, in Giskard.precommit]
b:17 [binder, in Giskard.precommit]
b:18 [binder, in Giskard.structures]
b:207 [binder, in Giskard.global]
b:21 [binder, in Giskard.precommit]
b:215 [binder, in Giskard.global]
b:220 [binder, in Giskard.global]
b:221 [binder, in Giskard.local]
b:224 [binder, in Giskard.precommit]
b:224 [binder, in Giskard.global]
b:224 [binder, in Giskard.local]
b:227 [binder, in Giskard.precommit]
b:227 [binder, in Giskard.local]
b:229 [binder, in Giskard.global]
b:230 [binder, in Giskard.local]
b:238 [binder, in Giskard.global]
b:25 [binder, in Giskard.structures]
b:257 [binder, in Giskard.global]
b:26 [binder, in Giskard.precommit]
b:26 [binder, in Giskard.local]
b:260 [binder, in Giskard.precommit]
b:262 [binder, in Giskard.global]
b:269 [binder, in Giskard.global]
b:27 [binder, in Giskard.structures]
b:277 [binder, in Giskard.precommit]
b:277 [binder, in Giskard.global]
b:281 [binder, in Giskard.global]
b:29 [binder, in Giskard.structures]
b:30 [binder, in Giskard.precommit]
b:30 [binder, in Giskard.local]
b:33 [binder, in Giskard.local]
b:331 [binder, in Giskard.precommit]
b:35 [binder, in Giskard.precommit]
b:35 [binder, in Giskard.local]
b:37 [binder, in Giskard.local]
b:4 [binder, in Giskard.commit]
b:4 [binder, in Giskard.precommit]
b:40 [binder, in Giskard.precommit]
b:40 [binder, in Giskard.local]
b:42 [binder, in Giskard.local]
b:44 [binder, in Giskard.precommit]
b:44 [binder, in Giskard.local]
b:47 [binder, in Giskard.local]
b:49 [binder, in Giskard.precommit]
b:5 [binder, in Giskard.structures]
b:51 [binder, in Giskard.local]
b:53 [binder, in Giskard.precommit]
b:54 [binder, in Giskard.local]
b:58 [binder, in Giskard.precommit]
b:58 [binder, in Giskard.local]
b:61 [binder, in Giskard.local]
b:63 [binder, in Giskard.precommit]
b:64 [binder, in Giskard.local]
b:68 [binder, in Giskard.precommit]
b:68 [binder, in Giskard.prepare]
b:7 [binder, in Giskard.structures]
b:78 [binder, in Giskard.precommit]
b:78 [binder, in Giskard.local]
b:8 [binder, in Giskard.precommit]
b:85 [binder, in Giskard.precommit]
b:96 [binder, in Giskard.precommit]
b:98 [binder, in Giskard.precommit]
C
commit [library]commit_height_injective [lemma, in Giskard.commit]
commit_height_injective_statement [definition, in Giskard.commit]
commit_stage [definition, in Giskard.commit]
counting_messages_inclusion [lemma, in Giskard.global]
counting_message_change_view_change [lemma, in Giskard.global]
counting_message_different_tells_receiver [lemma, in Giskard.global]
counting_messages_monotonic [lemma, in Giskard.global]
counting_messages_change_tells_receiver [lemma, in Giskard.global]
counting_messages [projection, in Giskard.structures]
counting_messages_local_monotonic [lemma, in Giskard.local]
counting_messages_same_view_monotonic [lemma, in Giskard.local]
D
delivered_means_sender_made_transition [lemma, in Giskard.global]delivered_means_sent_local [lemma, in Giskard.global]
delivered_means_sent_global [lemma, in Giskard.global]
discard [definition, in Giskard.local]
discard_view_invalid_type [constructor, in Giskard.local]
discard_view_invalid [definition, in Giskard.local]
E
empty_has_no_one_third [lemma, in Giskard.structures]empty_has_no_one_third' [axiom, in Giskard.structures]
empty_has_no_two_thirds [lemma, in Giskard.structures]
empty_has_no_two_thirds' [axiom, in Giskard.structures]
equivocating_messages [definition, in Giskard.local]
equivocating_in_global_state [definition, in Giskard.prepare]
equivocating_in_state [definition, in Giskard.prepare]
eq_dec:4 [binder, in Giskard.lib]
evil_participants [axiom, in Giskard.structures]
exists_max_prepare_height_in_view_global [definition, in Giskard.precommit]
exists_same_height_block_correct [lemma, in Giskard.local]
exists_same_height_blockb [definition, in Giskard.local]
exists_same_height_block_dec [definition, in Giskard.local]
exists_same_height_PrepareBlock [definition, in Giskard.local]
exists_same_height_block [definition, in Giskard.local]
exists_same_height_block_old [definition, in Giskard.local]
F
flip_timeout [definition, in Giskard.local]G
generate_new_block_parent [axiom, in Giskard.structures]generate_last_block [axiom, in Giskard.structures]
generate_new_block [axiom, in Giskard.structures]
GenesisBlock [axiom, in Giskard.structures]
GenesisBlock_height [axiom, in Giskard.structures]
GenesisBlock_message [definition, in Giskard.local]
get_piggyback_block [projection, in Giskard.structures]
get_block [projection, in Giskard.structures]
get_sender [projection, in Giskard.structures]
get_view [projection, in Giskard.structures]
get_message_type [projection, in Giskard.structures]
get_transition [definition, in Giskard.local]
get_view_highest_ViewChange_message_in_counting_messages [lemma, in Giskard.local]
get_view_highest_ViewChange_message_node_view [lemma, in Giskard.local]
global [library]
global_local_out_if [lemma, in Giskard.global]
global_messages_monotonic [lemma, in Giskard.global]
global_messages_monotonic_step [lemma, in Giskard.global]
global_equivocating_local [lemma, in Giskard.prepare]
GState [definition, in Giskard.global]
GState_init_protocol_state [lemma, in Giskard.global]
GState_sane_transition [lemma, in Giskard.global]
GState_init_sane [lemma, in Giskard.global]
GState_sane [definition, in Giskard.global]
GState_step_transition [lemma, in Giskard.global]
GState_transition [definition, in Giskard.global]
GState_step_timeout [constructor, in Giskard.global]
GState_step_process [constructor, in Giskard.global]
GState_step [inductive, in Giskard.global]
GState_init [definition, in Giskard.global]
GTrace [definition, in Giskard.global]
g':14 [binder, in Giskard.global]
g':16 [binder, in Giskard.global]
g':19 [binder, in Giskard.global]
g':26 [binder, in Giskard.global]
g':30 [binder, in Giskard.global]
g:13 [binder, in Giskard.global]
g:15 [binder, in Giskard.global]
g:18 [binder, in Giskard.global]
g:2 [binder, in Giskard.global]
g:25 [binder, in Giskard.global]
g:27 [binder, in Giskard.global]
g:29 [binder, in Giskard.global]
g:33 [binder, in Giskard.global]
H
has_at_least_one_third [definition, in Giskard.structures]has_at_least_one_thirdb [axiom, in Giskard.structures]
has_at_least_two_thirds [definition, in Giskard.structures]
has_at_least_two_thirdsb [axiom, in Giskard.structures]
higher_block [definition, in Giskard.structures]
higher_message [definition, in Giskard.local]
highest_ViewChange_message_type_eq_ViewChange [lemma, in Giskard.local]
highest_ViewChange_message [definition, in Giskard.local]
highest_message_in_list [definition, in Giskard.local]
highest_msg:104 [binder, in Giskard.local]
highest_prepare_block_message [definition, in Giskard.local]
highest_prepare_block_in_view [definition, in Giskard.local]
highest_ViewChange_block_height_in_view [definition, in Giskard.local]
highest_ViewChange_block_in_view [definition, in Giskard.local]
honest_nodeb_correct [axiom, in Giskard.structures]
honest_nodeb [axiom, in Giskard.structures]
honest_node [axiom, in Giskard.structures]
h_max:357 [binder, in Giskard.precommit]
h_max:352 [binder, in Giskard.precommit]
h_max:326 [binder, in Giskard.precommit]
h_max:292 [binder, in Giskard.precommit]
h_max:287 [binder, in Giskard.precommit]
h_max:282 [binder, in Giskard.precommit]
H_prot:264 [binder, in Giskard.precommit]
h_local:123 [binder, in Giskard.precommit]
h:102 [binder, in Giskard.precommit]
h:109 [binder, in Giskard.precommit]
h:117 [binder, in Giskard.precommit]
h:120 [binder, in Giskard.precommit]
h:126 [binder, in Giskard.precommit]
h:133 [binder, in Giskard.precommit]
h:140 [binder, in Giskard.precommit]
h:329 [binder, in Giskard.precommit]
h:342 [binder, in Giskard.precommit]
h:95 [binder, in Giskard.precommit]
I
increment_view [definition, in Giskard.local]intersection_property [axiom, in Giskard.structures]
in_messages [projection, in Giskard.structures]
is_max_prepare_height_in_view_disj_global [lemma, in Giskard.precommit]
is_min_prepare_height_in_view [definition, in Giskard.precommit]
is_min_prepare_height_in_view_global [definition, in Giskard.precommit]
is_min_prepare_height_global [definition, in Giskard.precommit]
is_max_prepare_height_in_view [definition, in Giskard.precommit]
is_max_prepare_height_in_view_global [definition, in Giskard.precommit]
is_max_prepare_height_global [definition, in Giskard.precommit]
is_new_proposer_unique [axiom, in Giskard.structures]
is_block_proposer [axiom, in Giskard.structures]
is_member_correct [lemma, in Giskard.structures]
is_member [definition, in Giskard.structures]
i_past:178 [binder, in Giskard.global]
i_past:110 [binder, in Giskard.global]
i1:180 [binder, in Giskard.global]
i1:44 [binder, in Giskard.global]
i2:181 [binder, in Giskard.global]
i2:45 [binder, in Giskard.global]
i:101 [binder, in Giskard.precommit]
i:103 [binder, in Giskard.global]
i:107 [binder, in Giskard.precommit]
i:107 [binder, in Giskard.global]
i:11 [binder, in Giskard.precommit]
i:112 [binder, in Giskard.global]
i:114 [binder, in Giskard.precommit]
i:116 [binder, in Giskard.global]
i:119 [binder, in Giskard.precommit]
i:120 [binder, in Giskard.global]
i:125 [binder, in Giskard.precommit]
i:127 [binder, in Giskard.global]
i:13 [binder, in Giskard.prepare]
i:132 [binder, in Giskard.precommit]
i:135 [binder, in Giskard.global]
i:138 [binder, in Giskard.precommit]
i:142 [binder, in Giskard.global]
i:145 [binder, in Giskard.precommit]
i:15 [binder, in Giskard.precommit]
i:150 [binder, in Giskard.precommit]
i:153 [binder, in Giskard.global]
i:156 [binder, in Giskard.precommit]
i:157 [binder, in Giskard.global]
i:162 [binder, in Giskard.precommit]
i:162 [binder, in Giskard.global]
i:165 [binder, in Giskard.global]
i:168 [binder, in Giskard.precommit]
i:170 [binder, in Giskard.global]
i:174 [binder, in Giskard.precommit]
i:175 [binder, in Giskard.global]
i:178 [binder, in Giskard.precommit]
i:182 [binder, in Giskard.precommit]
i:184 [binder, in Giskard.global]
i:186 [binder, in Giskard.precommit]
i:188 [binder, in Giskard.global]
i:191 [binder, in Giskard.precommit]
i:193 [binder, in Giskard.global]
i:195 [binder, in Giskard.precommit]
i:197 [binder, in Giskard.global]
i:199 [binder, in Giskard.precommit]
i:2 [binder, in Giskard.commit]
i:2 [binder, in Giskard.precommit]
i:2 [binder, in Giskard.prepare]
i:20 [binder, in Giskard.precommit]
i:201 [binder, in Giskard.global]
i:206 [binder, in Giskard.global]
i:208 [binder, in Giskard.precommit]
i:21 [binder, in Giskard.prepare]
i:212 [binder, in Giskard.precommit]
i:214 [binder, in Giskard.global]
i:216 [binder, in Giskard.precommit]
i:219 [binder, in Giskard.global]
i:220 [binder, in Giskard.precommit]
i:223 [binder, in Giskard.global]
i:226 [binder, in Giskard.precommit]
i:228 [binder, in Giskard.global]
i:231 [binder, in Giskard.precommit]
i:236 [binder, in Giskard.precommit]
i:237 [binder, in Giskard.global]
i:24 [binder, in Giskard.prepare]
i:240 [binder, in Giskard.precommit]
i:245 [binder, in Giskard.precommit]
i:248 [binder, in Giskard.global]
i:25 [binder, in Giskard.precommit]
i:251 [binder, in Giskard.precommit]
i:251 [binder, in Giskard.global]
i:255 [binder, in Giskard.precommit]
i:256 [binder, in Giskard.global]
i:259 [binder, in Giskard.precommit]
i:261 [binder, in Giskard.global]
i:265 [binder, in Giskard.precommit]
i:268 [binder, in Giskard.global]
i:27 [binder, in Giskard.prepare]
i:270 [binder, in Giskard.precommit]
i:273 [binder, in Giskard.precommit]
i:276 [binder, in Giskard.global]
i:279 [binder, in Giskard.precommit]
i:284 [binder, in Giskard.precommit]
i:289 [binder, in Giskard.precommit]
i:29 [binder, in Giskard.precommit]
i:295 [binder, in Giskard.precommit]
i:299 [binder, in Giskard.precommit]
i:304 [binder, in Giskard.precommit]
i:309 [binder, in Giskard.precommit]
i:313 [binder, in Giskard.precommit]
i:318 [binder, in Giskard.precommit]
i:32 [binder, in Giskard.prepare]
i:323 [binder, in Giskard.precommit]
i:328 [binder, in Giskard.precommit]
i:333 [binder, in Giskard.precommit]
i:34 [binder, in Giskard.precommit]
i:341 [binder, in Giskard.precommit]
i:349 [binder, in Giskard.precommit]
i:354 [binder, in Giskard.precommit]
i:359 [binder, in Giskard.precommit]
i:364 [binder, in Giskard.precommit]
i:37 [binder, in Giskard.prepare]
i:381 [binder, in Giskard.precommit]
i:387 [binder, in Giskard.precommit]
i:39 [binder, in Giskard.precommit]
i:393 [binder, in Giskard.precommit]
i:40 [binder, in Giskard.prepare]
i:41 [binder, in Giskard.global]
i:43 [binder, in Giskard.precommit]
i:47 [binder, in Giskard.precommit]
i:47 [binder, in Giskard.prepare]
i:48 [binder, in Giskard.global]
i:49 [binder, in Giskard.prepare]
i:52 [binder, in Giskard.precommit]
i:56 [binder, in Giskard.global]
i:57 [binder, in Giskard.precommit]
i:61 [binder, in Giskard.precommit]
i:62 [binder, in Giskard.prepare]
i:65 [binder, in Giskard.global]
i:66 [binder, in Giskard.precommit]
i:67 [binder, in Giskard.prepare]
i:7 [binder, in Giskard.commit]
i:7 [binder, in Giskard.precommit]
i:70 [binder, in Giskard.precommit]
i:71 [binder, in Giskard.prepare]
i:74 [binder, in Giskard.prepare]
i:76 [binder, in Giskard.precommit]
i:80 [binder, in Giskard.global]
i:83 [binder, in Giskard.precommit]
i:85 [binder, in Giskard.global]
i:88 [binder, in Giskard.precommit]
i:89 [binder, in Giskard.global]
i:94 [binder, in Giskard.precommit]
i:96 [binder, in Giskard.global]
J
j:166 [binder, in Giskard.global]j:171 [binder, in Giskard.global]
j:208 [binder, in Giskard.global]
j:231 [binder, in Giskard.global]
j:264 [binder, in Giskard.global]
j:272 [binder, in Giskard.global]
j:279 [binder, in Giskard.global]
j:370 [binder, in Giskard.precommit]
j:375 [binder, in Giskard.precommit]
j:41 [binder, in Giskard.precommit]
j:48 [binder, in Giskard.precommit]
L
last_block_highest_block_global [lemma, in Giskard.precommit]last_block_highest_block_sent [lemma, in Giskard.precommit]
last_block [definition, in Giskard.local]
le_S_disj [lemma, in Giskard.lib]
lib [library]
lift_sent_to_received [lemma, in Giskard.global]
lm0:101 [binder, in Giskard.global]
lm0:123 [binder, in Giskard.global]
lm0:131 [binder, in Giskard.global]
lm0:138 [binder, in Giskard.global]
lm0:206 [binder, in Giskard.precommit]
lm0:52 [binder, in Giskard.global]
lm0:69 [binder, in Giskard.global]
lm0:83 [binder, in Giskard.global]
lm0:94 [binder, in Giskard.global]
lm1:119 [binder, in Giskard.structures]
lm2:120 [binder, in Giskard.structures]
lm:109 [binder, in Giskard.local]
lm:113 [binder, in Giskard.local]
lm:117 [binder, in Giskard.structures]
lm:117 [binder, in Giskard.local]
lm:118 [binder, in Giskard.structures]
lm:12 [binder, in Giskard.global]
lm:12 [binder, in Giskard.local]
lm:121 [binder, in Giskard.local]
lm:123 [binder, in Giskard.structures]
lm:125 [binder, in Giskard.local]
lm:129 [binder, in Giskard.local]
lm:133 [binder, in Giskard.local]
lm:137 [binder, in Giskard.local]
lm:141 [binder, in Giskard.local]
lm:145 [binder, in Giskard.local]
lm:149 [binder, in Giskard.local]
lm:154 [binder, in Giskard.local]
lm:157 [binder, in Giskard.local]
lm:174 [binder, in Giskard.local]
lm:178 [binder, in Giskard.local]
lm:182 [binder, in Giskard.local]
lm:187 [binder, in Giskard.local]
lm:191 [binder, in Giskard.local]
lm:199 [binder, in Giskard.local]
lm:205 [binder, in Giskard.local]
lm:211 [binder, in Giskard.local]
lm:217 [binder, in Giskard.local]
lm:228 [binder, in Giskard.local]
lm:23 [binder, in Giskard.global]
lm:231 [binder, in Giskard.local]
lm:336 [binder, in Giskard.precommit]
lm:344 [binder, in Giskard.precommit]
lm:5 [binder, in Giskard.global]
lm:8 [binder, in Giskard.local]
ln:73 [binder, in Giskard.structures]
local [library]
local_leq_global [lemma, in Giskard.precommit]
local_global_out_if [lemma, in Giskard.global]
local_evidence_of_equivocation [lemma, in Giskard.prepare]
l_superset:60 [binder, in Giskard.structures]
l1:65 [binder, in Giskard.structures]
l2:66 [binder, in Giskard.structures]
l:47 [binder, in Giskard.structures]
l:49 [binder, in Giskard.structures]
l:5 [binder, in Giskard.lib]
l:50 [binder, in Giskard.structures]
l:53 [binder, in Giskard.structures]
l:56 [binder, in Giskard.structures]
l:59 [binder, in Giskard.structures]
l:64 [binder, in Giskard.structures]
l:67 [binder, in Giskard.structures]
M
majority_shrink [lemma, in Giskard.structures]majority_growth [axiom, in Giskard.structures]
make_PrepareBlocks_message_type [lemma, in Giskard.global]
make_ViewChangeQC [definition, in Giskard.local]
make_ViewChange [definition, in Giskard.local]
make_PrepareQC [definition, in Giskard.local]
make_PrepareVote [definition, in Giskard.local]
make_PrepareBlocks_message_type [lemma, in Giskard.local]
make_PrepareBlocks [definition, in Giskard.local]
malicious_ignore [definition, in Giskard.local]
message [record, in Giskard.structures]
message_type_PrepareVote [lemma, in Giskard.global]
message_with_higher_block [definition, in Giskard.structures]
message_eqb_correct [lemma, in Giskard.structures]
message_eqb [definition, in Giskard.structures]
message_eq_dec [definition, in Giskard.structures]
message_type_eqb_correct [lemma, in Giskard.structures]
message_type_eqb [definition, in Giskard.structures]
message_type_eq_dec [definition, in Giskard.structures]
message_type [inductive, in Giskard.structures]
minority_subset [axiom, in Giskard.structures]
modus_tollens [lemma, in Giskard.lib]
msg':15 [binder, in Giskard.prepare]
msg':203 [binder, in Giskard.global]
msg':302 [binder, in Giskard.precommit]
msg':316 [binder, in Giskard.precommit]
msg':321 [binder, in Giskard.precommit]
msg':362 [binder, in Giskard.precommit]
msg':368 [binder, in Giskard.precommit]
msg0:100 [binder, in Giskard.global]
msg0:125 [binder, in Giskard.global]
msg0:130 [binder, in Giskard.global]
msg0:140 [binder, in Giskard.global]
msg0:201 [binder, in Giskard.local]
msg0:205 [binder, in Giskard.precommit]
msg0:207 [binder, in Giskard.local]
msg0:213 [binder, in Giskard.local]
msg0:219 [binder, in Giskard.local]
msg0:245 [binder, in Giskard.global]
msg0:346 [binder, in Giskard.precommit]
msg0:51 [binder, in Giskard.global]
msg0:68 [binder, in Giskard.global]
msg0:88 [binder, in Giskard.local]
msg0:93 [binder, in Giskard.global]
msg0:98 [binder, in Giskard.local]
msg1:115 [binder, in Giskard.structures]
msg1:150 [binder, in Giskard.local]
msg1:159 [binder, in Giskard.global]
msg1:17 [binder, in Giskard.prepare]
msg1:229 [binder, in Giskard.precommit]
msg1:23 [binder, in Giskard.local]
msg1:233 [binder, in Giskard.precommit]
msg1:237 [binder, in Giskard.precommit]
msg1:242 [binder, in Giskard.precommit]
msg1:247 [binder, in Giskard.precommit]
msg1:252 [binder, in Giskard.precommit]
msg1:256 [binder, in Giskard.precommit]
msg1:28 [binder, in Giskard.prepare]
msg1:33 [binder, in Giskard.prepare]
msg1:372 [binder, in Giskard.precommit]
msg1:378 [binder, in Giskard.precommit]
msg1:43 [binder, in Giskard.prepare]
msg1:55 [binder, in Giskard.precommit]
msg1:9 [binder, in Giskard.prepare]
msg2:10 [binder, in Giskard.prepare]
msg2:116 [binder, in Giskard.structures]
msg2:151 [binder, in Giskard.local]
msg2:18 [binder, in Giskard.prepare]
msg2:234 [binder, in Giskard.precommit]
msg2:238 [binder, in Giskard.precommit]
msg2:24 [binder, in Giskard.local]
msg2:243 [binder, in Giskard.precommit]
msg2:249 [binder, in Giskard.precommit]
msg2:253 [binder, in Giskard.precommit]
msg2:257 [binder, in Giskard.precommit]
msg2:29 [binder, in Giskard.prepare]
msg2:34 [binder, in Giskard.prepare]
msg2:373 [binder, in Giskard.precommit]
msg2:379 [binder, in Giskard.precommit]
msg2:44 [binder, in Giskard.prepare]
msg:101 [binder, in Giskard.local]
msg:105 [binder, in Giskard.global]
msg:107 [binder, in Giskard.local]
msg:109 [binder, in Giskard.global]
msg:11 [binder, in Giskard.global]
msg:111 [binder, in Giskard.local]
msg:114 [binder, in Giskard.global]
msg:115 [binder, in Giskard.local]
msg:118 [binder, in Giskard.global]
msg:119 [binder, in Giskard.local]
msg:121 [binder, in Giskard.global]
msg:121 [binder, in Giskard.structures]
msg:123 [binder, in Giskard.local]
msg:124 [binder, in Giskard.structures]
msg:127 [binder, in Giskard.local]
msg:131 [binder, in Giskard.local]
msg:133 [binder, in Giskard.global]
msg:135 [binder, in Giskard.local]
msg:136 [binder, in Giskard.global]
msg:139 [binder, in Giskard.local]
msg:14 [binder, in Giskard.prepare]
msg:143 [binder, in Giskard.global]
msg:143 [binder, in Giskard.local]
msg:145 [binder, in Giskard.global]
msg:146 [binder, in Giskard.global]
msg:147 [binder, in Giskard.global]
msg:147 [binder, in Giskard.local]
msg:148 [binder, in Giskard.global]
msg:149 [binder, in Giskard.global]
msg:150 [binder, in Giskard.global]
msg:151 [binder, in Giskard.global]
msg:154 [binder, in Giskard.global]
msg:158 [binder, in Giskard.local]
msg:16 [binder, in Giskard.local]
msg:161 [binder, in Giskard.local]
msg:162 [binder, in Giskard.local]
msg:164 [binder, in Giskard.local]
msg:165 [binder, in Giskard.local]
msg:166 [binder, in Giskard.local]
msg:168 [binder, in Giskard.global]
msg:168 [binder, in Giskard.local]
msg:169 [binder, in Giskard.local]
msg:170 [binder, in Giskard.local]
msg:172 [binder, in Giskard.local]
msg:176 [binder, in Giskard.precommit]
msg:176 [binder, in Giskard.local]
msg:180 [binder, in Giskard.precommit]
msg:180 [binder, in Giskard.local]
msg:184 [binder, in Giskard.precommit]
msg:185 [binder, in Giskard.global]
msg:185 [binder, in Giskard.local]
msg:188 [binder, in Giskard.precommit]
msg:189 [binder, in Giskard.global]
msg:189 [binder, in Giskard.local]
msg:19 [binder, in Giskard.local]
msg:192 [binder, in Giskard.precommit]
msg:194 [binder, in Giskard.global]
msg:197 [binder, in Giskard.precommit]
msg:198 [binder, in Giskard.global]
msg:198 [binder, in Giskard.local]
msg:202 [binder, in Giskard.precommit]
msg:202 [binder, in Giskard.global]
msg:204 [binder, in Giskard.local]
msg:209 [binder, in Giskard.global]
msg:21 [binder, in Giskard.local]
msg:210 [binder, in Giskard.precommit]
msg:210 [binder, in Giskard.global]
msg:210 [binder, in Giskard.local]
msg:211 [binder, in Giskard.global]
msg:212 [binder, in Giskard.global]
msg:214 [binder, in Giskard.precommit]
msg:216 [binder, in Giskard.local]
msg:217 [binder, in Giskard.global]
msg:218 [binder, in Giskard.precommit]
msg:22 [binder, in Giskard.global]
msg:221 [binder, in Giskard.global]
msg:222 [binder, in Giskard.local]
msg:223 [binder, in Giskard.precommit]
msg:225 [binder, in Giskard.local]
msg:23 [binder, in Giskard.precommit]
msg:232 [binder, in Giskard.global]
msg:232 [binder, in Giskard.local]
msg:233 [binder, in Giskard.global]
msg:234 [binder, in Giskard.global]
msg:235 [binder, in Giskard.global]
msg:240 [binder, in Giskard.global]
msg:241 [binder, in Giskard.global]
msg:242 [binder, in Giskard.global]
msg:243 [binder, in Giskard.global]
msg:246 [binder, in Giskard.global]
msg:249 [binder, in Giskard.global]
msg:262 [binder, in Giskard.precommit]
msg:263 [binder, in Giskard.global]
msg:265 [binder, in Giskard.global]
msg:266 [binder, in Giskard.precommit]
msg:27 [binder, in Giskard.local]
msg:271 [binder, in Giskard.precommit]
msg:271 [binder, in Giskard.global]
msg:273 [binder, in Giskard.global]
msg:276 [binder, in Giskard.precommit]
msg:28 [binder, in Giskard.local]
msg:281 [binder, in Giskard.precommit]
msg:286 [binder, in Giskard.precommit]
msg:291 [binder, in Giskard.precommit]
msg:296 [binder, in Giskard.precommit]
msg:301 [binder, in Giskard.precommit]
msg:307 [binder, in Giskard.precommit]
msg:31 [binder, in Giskard.local]
msg:311 [binder, in Giskard.precommit]
msg:315 [binder, in Giskard.precommit]
msg:32 [binder, in Giskard.precommit]
msg:320 [binder, in Giskard.precommit]
msg:325 [binder, in Giskard.precommit]
msg:335 [binder, in Giskard.precommit]
msg:337 [binder, in Giskard.precommit]
msg:338 [binder, in Giskard.precommit]
msg:34 [binder, in Giskard.local]
msg:345 [binder, in Giskard.precommit]
msg:351 [binder, in Giskard.precommit]
msg:356 [binder, in Giskard.precommit]
msg:36 [binder, in Giskard.local]
msg:361 [binder, in Giskard.precommit]
msg:366 [binder, in Giskard.precommit]
msg:38 [binder, in Giskard.local]
msg:48 [binder, in Giskard.local]
msg:54 [binder, in Giskard.global]
msg:55 [binder, in Giskard.local]
msg:58 [binder, in Giskard.global]
msg:62 [binder, in Giskard.local]
msg:63 [binder, in Giskard.global]
msg:68 [binder, in Giskard.local]
msg:71 [binder, in Giskard.global]
msg:71 [binder, in Giskard.local]
msg:72 [binder, in Giskard.prepare]
msg:74 [binder, in Giskard.global]
msg:78 [binder, in Giskard.global]
msg:83 [binder, in Giskard.local]
msg:87 [binder, in Giskard.global]
msg:89 [binder, in Giskard.local]
msg:95 [binder, in Giskard.local]
msg:99 [binder, in Giskard.local]
mt1:79 [binder, in Giskard.structures]
mt1:81 [binder, in Giskard.structures]
mt1:83 [binder, in Giskard.structures]
mt2:80 [binder, in Giskard.structures]
mt2:82 [binder, in Giskard.structures]
mt2:84 [binder, in Giskard.structures]
m1:91 [binder, in Giskard.structures]
m1:93 [binder, in Giskard.structures]
m1:95 [binder, in Giskard.structures]
m2:92 [binder, in Giskard.structures]
m2:94 [binder, in Giskard.structures]
m2:96 [binder, in Giskard.structures]
m:10 [binder, in Giskard.local]
m:11 [binder, in Giskard.lib]
m:14 [binder, in Giskard.local]
m:170 [binder, in Giskard.precommit]
m:2 [binder, in Giskard.local]
m:383 [binder, in Giskard.precommit]
m:389 [binder, in Giskard.precommit]
m:395 [binder, in Giskard.precommit]
m:4 [binder, in Giskard.local]
m:4 [binder, in Giskard.prepare]
m:50 [binder, in Giskard.global]
m:6 [binder, in Giskard.local]
m:72 [binder, in Giskard.precommit]
m:9 [binder, in Giskard.commit]
m:90 [binder, in Giskard.precommit]
m:92 [binder, in Giskard.global]
m:99 [binder, in Giskard.global]
N
node [axiom, in Giskard.structures]node_id [projection, in Giskard.structures]
node_view [projection, in Giskard.structures]
node_eq_dec [definition, in Giskard.structures]
node_eqb_no [lemma, in Giskard.structures]
node_eqb_comm [lemma, in Giskard.structures]
node_eqb_refl [lemma, in Giskard.structures]
node_eqb_correct [axiom, in Giskard.structures]
node_eqb [axiom, in Giskard.structures]
normal_trigger_message_highest_global [lemma, in Giskard.precommit]
normal_trigger_message_highest_global_statement [definition, in Giskard.precommit]
normal_trigger_message_global [definition, in Giskard.precommit]
not_my_problem [lemma, in Giskard.global]
not_prepare_stage [lemma, in Giskard.local]
no_prepare_blocks_GState_init [lemma, in Giskard.global]
NState [record, in Giskard.structures]
NState_eq_dec [definition, in Giskard.structures]
NState_init [definition, in Giskard.structures]
NState_transition_type [inductive, in Giskard.local]
ns:71 [binder, in Giskard.structures]
n':248 [binder, in Giskard.precommit]
n0:122 [binder, in Giskard.global]
n0:128 [binder, in Giskard.global]
n0:137 [binder, in Giskard.global]
n0:203 [binder, in Giskard.precommit]
n0:66 [binder, in Giskard.global]
n0:82 [binder, in Giskard.global]
n1:108 [binder, in Giskard.structures]
n1:32 [binder, in Giskard.structures]
n1:36 [binder, in Giskard.structures]
n1:38 [binder, in Giskard.structures]
n1:40 [binder, in Giskard.structures]
n1:60 [binder, in Giskard.global]
n1:76 [binder, in Giskard.global]
n2:109 [binder, in Giskard.structures]
n2:33 [binder, in Giskard.structures]
n2:37 [binder, in Giskard.structures]
n2:39 [binder, in Giskard.structures]
n2:41 [binder, in Giskard.structures]
n2:61 [binder, in Giskard.global]
n2:77 [binder, in Giskard.global]
n:1 [binder, in Giskard.global]
n:10 [binder, in Giskard.lib]
n:104 [binder, in Giskard.global]
n:104 [binder, in Giskard.structures]
n:108 [binder, in Giskard.precommit]
n:108 [binder, in Giskard.global]
n:113 [binder, in Giskard.global]
n:117 [binder, in Giskard.global]
n:12 [binder, in Giskard.precommit]
n:12 [binder, in Giskard.prepare]
n:122 [binder, in Giskard.precommit]
n:132 [binder, in Giskard.global]
n:139 [binder, in Giskard.precommit]
n:144 [binder, in Giskard.global]
n:152 [binder, in Giskard.local]
n:155 [binder, in Giskard.global]
n:155 [binder, in Giskard.local]
n:158 [binder, in Giskard.global]
n:16 [binder, in Giskard.precommit]
n:163 [binder, in Giskard.precommit]
n:163 [binder, in Giskard.global]
n:167 [binder, in Giskard.global]
n:169 [binder, in Giskard.precommit]
n:17 [binder, in Giskard.global]
n:172 [binder, in Giskard.global]
n:176 [binder, in Giskard.global]
n:182 [binder, in Giskard.global]
n:187 [binder, in Giskard.global]
n:190 [binder, in Giskard.precommit]
n:192 [binder, in Giskard.global]
n:194 [binder, in Giskard.precommit]
n:196 [binder, in Giskard.global]
n:20 [binder, in Giskard.global]
n:20 [binder, in Giskard.prepare]
n:200 [binder, in Giskard.global]
n:201 [binder, in Giskard.precommit]
n:205 [binder, in Giskard.global]
n:221 [binder, in Giskard.precommit]
n:227 [binder, in Giskard.global]
n:23 [binder, in Giskard.prepare]
n:232 [binder, in Giskard.precommit]
n:24 [binder, in Giskard.global]
n:241 [binder, in Giskard.precommit]
n:246 [binder, in Giskard.precommit]
n:252 [binder, in Giskard.global]
n:26 [binder, in Giskard.prepare]
n:260 [binder, in Giskard.global]
n:267 [binder, in Giskard.global]
n:274 [binder, in Giskard.precommit]
n:275 [binder, in Giskard.global]
n:28 [binder, in Giskard.global]
n:280 [binder, in Giskard.global]
n:294 [binder, in Giskard.precommit]
n:298 [binder, in Giskard.precommit]
n:3 [binder, in Giskard.commit]
n:3 [binder, in Giskard.precommit]
n:3 [binder, in Giskard.prepare]
n:306 [binder, in Giskard.precommit]
n:31 [binder, in Giskard.prepare]
n:32 [binder, in Giskard.global]
n:339 [binder, in Giskard.precommit]
n:347 [binder, in Giskard.precommit]
n:35 [binder, in Giskard.global]
n:35 [binder, in Giskard.structures]
n:36 [binder, in Giskard.prepare]
n:38 [binder, in Giskard.precommit]
n:382 [binder, in Giskard.precommit]
n:388 [binder, in Giskard.precommit]
n:39 [binder, in Giskard.global]
n:39 [binder, in Giskard.prepare]
n:394 [binder, in Giskard.precommit]
n:42 [binder, in Giskard.global]
n:42 [binder, in Giskard.prepare]
n:44 [binder, in Giskard.structures]
n:46 [binder, in Giskard.global]
n:46 [binder, in Giskard.prepare]
n:51 [binder, in Giskard.structures]
n:53 [binder, in Giskard.global]
n:53 [binder, in Giskard.prepare]
n:54 [binder, in Giskard.structures]
n:54 [binder, in Giskard.prepare]
n:55 [binder, in Giskard.prepare]
n:56 [binder, in Giskard.prepare]
n:57 [binder, in Giskard.global]
n:57 [binder, in Giskard.structures]
n:57 [binder, in Giskard.prepare]
n:58 [binder, in Giskard.prepare]
n:59 [binder, in Giskard.prepare]
n:6 [binder, in Giskard.global]
n:60 [binder, in Giskard.prepare]
n:61 [binder, in Giskard.structures]
n:62 [binder, in Giskard.precommit]
n:62 [binder, in Giskard.global]
n:63 [binder, in Giskard.structures]
n:63 [binder, in Giskard.prepare]
n:67 [binder, in Giskard.precommit]
n:68 [binder, in Giskard.structures]
n:70 [binder, in Giskard.global]
n:70 [binder, in Giskard.structures]
n:71 [binder, in Giskard.precommit]
n:72 [binder, in Giskard.structures]
n:73 [binder, in Giskard.global]
n:75 [binder, in Giskard.structures]
n:75 [binder, in Giskard.prepare]
n:77 [binder, in Giskard.precommit]
n:8 [binder, in Giskard.commit]
n:81 [binder, in Giskard.global]
n:84 [binder, in Giskard.precommit]
n:86 [binder, in Giskard.global]
n:89 [binder, in Giskard.precommit]
n:9 [binder, in Giskard.precommit]
n:9 [binder, in Giskard.global]
n:90 [binder, in Giskard.global]
n:97 [binder, in Giskard.global]
O
out_message_view_bound [lemma, in Giskard.precommit]out_message_change_tells_sender [lemma, in Giskard.global]
out_messages_change_means_sent [lemma, in Giskard.global]
out_messages_global_monotonic [lemma, in Giskard.global]
out_messages_global_monotonic_step [lemma, in Giskard.global]
out_messages [projection, in Giskard.structures]
out_messages_local_monotonic [lemma, in Giskard.local]
P
parent_block_height [axiom, in Giskard.structures]parent_ofb_correct [axiom, in Giskard.structures]
parent_ofb [axiom, in Giskard.structures]
parent_of [axiom, in Giskard.structures]
participants [axiom, in Giskard.structures]
participation_rights [lemma, in Giskard.global]
participation_rights_global [lemma, in Giskard.global]
past_view_trigger_message_lowest_block_global [lemma, in Giskard.precommit]
past_view_trigger_message_lowest_block_global_statement [definition, in Giskard.precommit]
past_view_exists_trigger_message_global [lemma, in Giskard.precommit]
pb_msg:268 [binder, in Giskard.precommit]
pending_PrepareVote_correct [lemma, in Giskard.local]
pending_PrepareVote [definition, in Giskard.local]
precommit [library]
precommit_now_height_injective [lemma, in Giskard.precommit]
precommit_now_height_injective_middle [definition, in Giskard.precommit]
precommit_now_height_injective_symmetric [lemma, in Giskard.precommit]
precommit_height_injective_symmetric [lemma, in Giskard.precommit]
precommit_stage_now_height_injective_statement [definition, in Giskard.precommit]
precommit_stage_now [definition, in Giskard.precommit]
precommit_stage_means_prepare_stage_global [lemma, in Giskard.precommit]
precommit_stage_height_injective_statement [definition, in Giskard.precommit]
precommit_means_prepare [lemma, in Giskard.precommit]
precommit_stage [definition, in Giskard.precommit]
prepare [library]
PrepareBlock [constructor, in Giskard.structures]
PrepareBlock_sender_view_injective_global [lemma, in Giskard.precommit]
PrepareBlock_sender_is_new_proposer_global [lemma, in Giskard.precommit]
PrepareBlock_sender_is_new_proposer_local [lemma, in Giskard.precommit]
PrepareBlock_block_height_geq [lemma, in Giskard.precommit]
prepareblock_msg:92 [binder, in Giskard.local]
PrepareQC [constructor, in Giskard.structures]
PrepareQC_sent_means_PrepareBlock_sent_global [lemma, in Giskard.precommit]
PrepareQC_sent_means_PrepareVote_sent_global [lemma, in Giskard.precommit]
PrepareQC_sent_means_exists_PrepareVote_processed_local [lemma, in Giskard.precommit]
PrepareQC_sent_means_exists_PrepareBlock_processed_local [definition, in Giskard.precommit]
PrepareQC_in_view_global [definition, in Giskard.precommit]
PrepareQC_in_view [definition, in Giskard.local]
PrepareQC_local_means_vote_quorum_global [lemma, in Giskard.prepare]
PrepareVote [constructor, in Giskard.structures]
PrepareVote_sent_means_PrepareBlock_sent_global [lemma, in Giskard.precommit]
PrepareVote_sent_means_PrepareBlock_processed_local [lemma, in Giskard.precommit]
PrepareVote_about_block_in_view_global [definition, in Giskard.precommit]
PrepareVote_about_block_global [definition, in Giskard.global]
PrepareVote_about_block_in_view_global [definition, in Giskard.global]
prepare_stage_in_view_means_PrepareBlock_sent_global [lemma, in Giskard.precommit]
prepare_means_PrepareVote_PrepareQC_exists_global [lemma, in Giskard.precommit]
prepare_stage_child_non_last [definition, in Giskard.precommit]
prepare_stage_height_view_morphism_global_non_last [definition, in Giskard.precommit]
prepare_stage_height_view_morphism_global [definition, in Giskard.precommit]
prepare_stage_first_parent_highest_or_second_global [definition, in Giskard.precommit]
prepare_stage_means_prepare_stage_global [lemma, in Giskard.precommit]
prepare_stage_in_view_means_prepare_stage_in_view_global [lemma, in Giskard.precommit]
prepare_stage_global [definition, in Giskard.precommit]
prepare_in_view_means_PrepareVote_PrepareQC_exists_global [lemma, in Giskard.precommit]
prepare_stage_in_view_persistent_global [lemma, in Giskard.precommit]
prepare_stage_in_view_step_global [lemma, in Giskard.precommit]
prepare_stage_persistent [lemma, in Giskard.precommit]
prepare_stage_in_view_global [definition, in Giskard.precommit]
prepare_stage_parent_prepare_stage [definition, in Giskard.precommit]
prepare_in_view_persistent [lemma, in Giskard.global]
prepare_stage_process_record_plural_agnostic [lemma, in Giskard.local]
prepare_stage_record_plural_agnostic [lemma, in Giskard.local]
prepare_stage_record_agnostic [lemma, in Giskard.local]
prepare_block_msg:96 [binder, in Giskard.local]
prepare_stage [definition, in Giskard.local]
prepare_stage_in_viewb [definition, in Giskard.local]
prepare_stage_in_view [definition, in Giskard.local]
prepare_stage_same_view_height_injective [lemma, in Giskard.prepare]
prepare_stage_same_view_height_injective_statement [definition, in Giskard.prepare]
previous_msg:86 [binder, in Giskard.local]
pre_local_evidence_of_equivocation [lemma, in Giskard.prepare]
pre_local_evidence_of_equivocation_last_case [lemma, in Giskard.prepare]
pre_local_evidence_of_equivocation_middle_case [lemma, in Giskard.prepare]
pre_local_evidence_of_equivocation_statement [definition, in Giskard.prepare]
pre_local_means_local_evidence_of_equivocation [lemma, in Giskard.prepare]
pre_equivocating_in_state [definition, in Giskard.prepare]
process [definition, in Giskard.local]
processed_means_sent_global [lemma, in Giskard.global]
processed_means_past_received [lemma, in Giskard.global]
processed_ViewChange_in_view_correct [lemma, in Giskard.local]
processed_ViewChange_in_view [definition, in Giskard.local]
processed_PrepareVote_in_view_about_block [definition, in Giskard.local]
process_PrepareBlock_malicious_vote_type [constructor, in Giskard.local]
process_ViewChangeQC_single_type [constructor, in Giskard.local]
process_ViewChange_pre_quorum_type [constructor, in Giskard.local]
process_ViewChange_quorum_new_proposer_type [constructor, in Giskard.local]
process_PrepareQC_non_last_block_type [constructor, in Giskard.local]
process_PrepareQC_last_block_type [constructor, in Giskard.local]
process_PrepareQC_last_block_new_proposer_type [constructor, in Giskard.local]
process_PrepareVote_wait_type [constructor, in Giskard.local]
process_PrepareVote_vote_type [constructor, in Giskard.local]
process_PrepareBlock_vote_type [constructor, in Giskard.local]
process_PrepareBlock_pending_vote_type [constructor, in Giskard.local]
process_PrepareBlock_duplicate_type [constructor, in Giskard.local]
process_PrepareBlock_malicious_vote [definition, in Giskard.local]
process_ViewChangeQC_single [definition, in Giskard.local]
process_ViewChange_pre_quorum [definition, in Giskard.local]
process_ViewChange_quorum_new_proposer [definition, in Giskard.local]
process_PrepareQC_non_last_block [definition, in Giskard.local]
process_PrepareQC_last_block [definition, in Giskard.local]
process_PrepareQC_last_block_new_proposer [definition, in Giskard.local]
process_PrepareVote_vote [definition, in Giskard.local]
process_PrepareVote_wait [definition, in Giskard.local]
process_PrepareBlock_vote [definition, in Giskard.local]
process_PrepareBlock_pending_vote [definition, in Giskard.local]
process_PrepareBlock_duplicate [definition, in Giskard.local]
process_timeout [definition, in Giskard.local]
process:10 [binder, in Giskard.global]
process:21 [binder, in Giskard.global]
propose_block_init_type [constructor, in Giskard.local]
propose_block_init [definition, in Giskard.local]
protocol_trace_state_sane [lemma, in Giskard.global]
protocol_trace_zero [lemma, in Giskard.global]
protocol_state [definition, in Giskard.global]
protocol_trace [definition, in Giskard.global]
p0:124 [binder, in Giskard.global]
p0:129 [binder, in Giskard.global]
p0:139 [binder, in Giskard.global]
p0:204 [binder, in Giskard.precommit]
p0:49 [binder, in Giskard.global]
p0:67 [binder, in Giskard.global]
p0:91 [binder, in Giskard.global]
p0:98 [binder, in Giskard.global]
p:103 [binder, in Giskard.precommit]
p:110 [binder, in Giskard.precommit]
p:115 [binder, in Giskard.precommit]
p:121 [binder, in Giskard.precommit]
p:128 [binder, in Giskard.precommit]
p:130 [binder, in Giskard.precommit]
p:134 [binder, in Giskard.precommit]
p:141 [binder, in Giskard.precommit]
p:175 [binder, in Giskard.precommit]
p:179 [binder, in Giskard.precommit]
p:18 [binder, in Giskard.precommit]
p:183 [binder, in Giskard.precommit]
p:187 [binder, in Giskard.precommit]
P:190 [binder, in Giskard.global]
p:200 [binder, in Giskard.precommit]
p:209 [binder, in Giskard.precommit]
p:213 [binder, in Giskard.precommit]
p:216 [binder, in Giskard.global]
p:217 [binder, in Giskard.precommit]
p:218 [binder, in Giskard.local]
p:22 [binder, in Giskard.precommit]
p:222 [binder, in Giskard.precommit]
p:225 [binder, in Giskard.global]
p:230 [binder, in Giskard.global]
p:239 [binder, in Giskard.global]
p:254 [binder, in Giskard.global]
p:258 [binder, in Giskard.global]
p:261 [binder, in Giskard.precommit]
p:27 [binder, in Giskard.precommit]
p:270 [binder, in Giskard.global]
p:275 [binder, in Giskard.precommit]
p:278 [binder, in Giskard.global]
p:280 [binder, in Giskard.precommit]
p:285 [binder, in Giskard.precommit]
p:290 [binder, in Giskard.precommit]
p:300 [binder, in Giskard.precommit]
p:305 [binder, in Giskard.precommit]
p:31 [binder, in Giskard.precommit]
p:310 [binder, in Giskard.precommit]
p:314 [binder, in Giskard.precommit]
p:319 [binder, in Giskard.precommit]
p:324 [binder, in Giskard.precommit]
p:330 [binder, in Giskard.precommit]
p:334 [binder, in Giskard.precommit]
p:343 [binder, in Giskard.precommit]
p:350 [binder, in Giskard.precommit]
p:355 [binder, in Giskard.precommit]
p:36 [binder, in Giskard.precommit]
p:45 [binder, in Giskard.precommit]
p:50 [binder, in Giskard.precommit]
p:52 [binder, in Giskard.prepare]
p:59 [binder, in Giskard.precommit]
p:64 [binder, in Giskard.precommit]
p:65 [binder, in Giskard.prepare]
p:69 [binder, in Giskard.prepare]
p:7 [binder, in Giskard.prepare]
p:77 [binder, in Giskard.prepare]
P:8 [binder, in Giskard.lib]
p:97 [binder, in Giskard.precommit]
p:99 [binder, in Giskard.precommit]
Q
qc_in_view_persistent [lemma, in Giskard.global]qc_current_view_persistent [lemma, in Giskard.global]
quorum [definition, in Giskard.structures]
quorumb [definition, in Giskard.structures]
quorum_growth [lemma, in Giskard.structures]
quorum_subset [axiom, in Giskard.structures]
quorum_msg:94 [binder, in Giskard.local]
quorum_msg:91 [binder, in Giskard.local]
Q:9 [binder, in Giskard.lib]
R
received [definition, in Giskard.local]record [definition, in Giskard.local]
record_plural [definition, in Giskard.local]
remove_subset [lemma, in Giskard.lib]
S
same_height_block_msg_dec [definition, in Giskard.local]same_height_block_msg [definition, in Giskard.local]
sent [definition, in Giskard.local]
sent_PrepareVote_means_parent_block_prepare_local [lemma, in Giskard.precommit]
sent_PrepareVote_means_received_PrepareBlock [lemma, in Giskard.global]
sent_PrepareVote_means_received_PrepareBlock [lemma, in Giskard.prepare]
state_view_morphism [lemma, in Giskard.global]
strongly_wedged_in_between [lemma, in Giskard.global]
structures [library]
s':108 [binder, in Giskard.local]
s':112 [binder, in Giskard.local]
s':116 [binder, in Giskard.local]
s':120 [binder, in Giskard.local]
s':124 [binder, in Giskard.local]
s':128 [binder, in Giskard.local]
s':132 [binder, in Giskard.local]
s':136 [binder, in Giskard.local]
s':140 [binder, in Giskard.local]
s':144 [binder, in Giskard.local]
s':148 [binder, in Giskard.local]
s':173 [binder, in Giskard.local]
s':177 [binder, in Giskard.local]
s':181 [binder, in Giskard.local]
s':186 [binder, in Giskard.local]
s':190 [binder, in Giskard.local]
s1:105 [binder, in Giskard.structures]
s1:196 [binder, in Giskard.local]
s1:202 [binder, in Giskard.local]
s1:208 [binder, in Giskard.local]
s1:214 [binder, in Giskard.local]
s1:3 [binder, in Giskard.global]
s2:106 [binder, in Giskard.structures]
s2:197 [binder, in Giskard.local]
s2:203 [binder, in Giskard.local]
s2:209 [binder, in Giskard.local]
s2:215 [binder, in Giskard.local]
s2:4 [binder, in Giskard.global]
s:1 [binder, in Giskard.local]
s:100 [binder, in Giskard.local]
s:102 [binder, in Giskard.local]
s:103 [binder, in Giskard.local]
s:105 [binder, in Giskard.local]
s:106 [binder, in Giskard.local]
s:11 [binder, in Giskard.local]
s:110 [binder, in Giskard.local]
s:114 [binder, in Giskard.local]
s:118 [binder, in Giskard.local]
s:122 [binder, in Giskard.local]
s:126 [binder, in Giskard.local]
s:13 [binder, in Giskard.local]
s:130 [binder, in Giskard.local]
s:134 [binder, in Giskard.local]
s:138 [binder, in Giskard.local]
s:142 [binder, in Giskard.local]
s:146 [binder, in Giskard.local]
s:15 [binder, in Giskard.local]
s:159 [binder, in Giskard.local]
s:16 [binder, in Giskard.prepare]
s:160 [binder, in Giskard.local]
s:163 [binder, in Giskard.local]
s:167 [binder, in Giskard.local]
s:17 [binder, in Giskard.local]
s:171 [binder, in Giskard.local]
s:175 [binder, in Giskard.local]
s:179 [binder, in Giskard.local]
s:18 [binder, in Giskard.local]
s:183 [binder, in Giskard.local]
s:184 [binder, in Giskard.local]
s:188 [binder, in Giskard.local]
s:20 [binder, in Giskard.local]
s:22 [binder, in Giskard.local]
s:220 [binder, in Giskard.local]
s:223 [binder, in Giskard.local]
s:226 [binder, in Giskard.local]
s:229 [binder, in Giskard.local]
s:244 [binder, in Giskard.global]
s:25 [binder, in Giskard.local]
s:29 [binder, in Giskard.local]
s:3 [binder, in Giskard.local]
s:32 [binder, in Giskard.local]
s:39 [binder, in Giskard.local]
s:41 [binder, in Giskard.local]
s:41 [binder, in Giskard.prepare]
s:43 [binder, in Giskard.local]
s:45 [binder, in Giskard.local]
s:49 [binder, in Giskard.local]
s:5 [binder, in Giskard.local]
s:52 [binder, in Giskard.local]
s:56 [binder, in Giskard.local]
s:59 [binder, in Giskard.local]
s:63 [binder, in Giskard.local]
s:66 [binder, in Giskard.local]
s:69 [binder, in Giskard.local]
s:7 [binder, in Giskard.local]
s:72 [binder, in Giskard.local]
s:74 [binder, in Giskard.local]
s:76 [binder, in Giskard.local]
s:79 [binder, in Giskard.local]
s:8 [binder, in Giskard.prepare]
s:84 [binder, in Giskard.local]
s:85 [binder, in Giskard.local]
s:87 [binder, in Giskard.local]
s:9 [binder, in Giskard.local]
s:90 [binder, in Giskard.local]
s:93 [binder, in Giskard.local]
s:97 [binder, in Giskard.local]
T
timeout [projection, in Giskard.structures]timeout_trigger_message_highest_or_second_highest_global [lemma, in Giskard.precommit]
timeout_trigger_message_at_least_second_highest_global [lemma, in Giskard.precommit]
timeout_trigger_message_global_means_exists_ViewChange_quorum [lemma, in Giskard.precommit]
timeout_trigger_message_highest_or_second_highest_global_statement [definition, in Giskard.precommit]
timeout_trigger_message_block_prepare_stage_global [lemma, in Giskard.precommit]
timeout_trigger_message_global_dec [definition, in Giskard.precommit]
timeout_trigger_message_global [definition, in Giskard.precommit]
trigger_message_view_morphism_global [lemma, in Giskard.precommit]
trigger_message_view_morphism_step_global [lemma, in Giskard.precommit]
trigger_message_past_exists_global [lemma, in Giskard.precommit]
trigger_message_past_step_exists_global [lemma, in Giskard.precommit]
trigger_message_highest_or_second_highest_global_statement [definition, in Giskard.precommit]
trigger_message_next_view_PrepareBlock_same_block_global [definition, in Giskard.precommit]
trigger_message_block_prepare_stage_global [lemma, in Giskard.precommit]
trigger_message_global_backwards_persistent_verbose [lemma, in Giskard.precommit]
trigger_message_global [definition, in Giskard.precommit]
tr:1 [binder, in Giskard.commit]
tr:1 [binder, in Giskard.precommit]
tr:1 [binder, in Giskard.prepare]
tr:10 [binder, in Giskard.precommit]
tr:100 [binder, in Giskard.precommit]
tr:102 [binder, in Giskard.global]
tr:106 [binder, in Giskard.precommit]
tr:106 [binder, in Giskard.global]
tr:11 [binder, in Giskard.prepare]
tr:111 [binder, in Giskard.global]
tr:113 [binder, in Giskard.precommit]
tr:115 [binder, in Giskard.global]
tr:118 [binder, in Giskard.precommit]
tr:119 [binder, in Giskard.global]
tr:124 [binder, in Giskard.precommit]
tr:126 [binder, in Giskard.global]
tr:131 [binder, in Giskard.precommit]
tr:134 [binder, in Giskard.global]
tr:137 [binder, in Giskard.precommit]
tr:14 [binder, in Giskard.precommit]
tr:141 [binder, in Giskard.global]
tr:144 [binder, in Giskard.precommit]
tr:149 [binder, in Giskard.precommit]
tr:152 [binder, in Giskard.global]
tr:155 [binder, in Giskard.precommit]
tr:156 [binder, in Giskard.global]
tr:161 [binder, in Giskard.precommit]
tr:161 [binder, in Giskard.global]
tr:164 [binder, in Giskard.global]
tr:167 [binder, in Giskard.precommit]
tr:169 [binder, in Giskard.global]
tr:173 [binder, in Giskard.precommit]
tr:174 [binder, in Giskard.global]
tr:177 [binder, in Giskard.precommit]
tr:179 [binder, in Giskard.global]
tr:181 [binder, in Giskard.precommit]
tr:183 [binder, in Giskard.global]
tr:185 [binder, in Giskard.precommit]
tr:186 [binder, in Giskard.global]
tr:189 [binder, in Giskard.precommit]
tr:19 [binder, in Giskard.precommit]
tr:19 [binder, in Giskard.prepare]
tr:191 [binder, in Giskard.global]
tr:193 [binder, in Giskard.precommit]
tr:195 [binder, in Giskard.global]
tr:198 [binder, in Giskard.precommit]
tr:199 [binder, in Giskard.global]
tr:204 [binder, in Giskard.global]
tr:207 [binder, in Giskard.precommit]
tr:211 [binder, in Giskard.precommit]
tr:213 [binder, in Giskard.global]
tr:215 [binder, in Giskard.precommit]
tr:218 [binder, in Giskard.global]
tr:219 [binder, in Giskard.precommit]
tr:22 [binder, in Giskard.prepare]
tr:222 [binder, in Giskard.global]
tr:225 [binder, in Giskard.precommit]
tr:226 [binder, in Giskard.global]
tr:230 [binder, in Giskard.precommit]
tr:235 [binder, in Giskard.precommit]
tr:236 [binder, in Giskard.global]
tr:239 [binder, in Giskard.precommit]
tr:24 [binder, in Giskard.precommit]
tr:244 [binder, in Giskard.precommit]
tr:247 [binder, in Giskard.global]
tr:25 [binder, in Giskard.prepare]
tr:250 [binder, in Giskard.precommit]
tr:250 [binder, in Giskard.global]
tr:254 [binder, in Giskard.precommit]
tr:255 [binder, in Giskard.global]
tr:258 [binder, in Giskard.precommit]
tr:259 [binder, in Giskard.global]
tr:263 [binder, in Giskard.precommit]
tr:266 [binder, in Giskard.global]
tr:269 [binder, in Giskard.precommit]
tr:272 [binder, in Giskard.precommit]
tr:274 [binder, in Giskard.global]
tr:278 [binder, in Giskard.precommit]
tr:28 [binder, in Giskard.precommit]
tr:283 [binder, in Giskard.precommit]
tr:288 [binder, in Giskard.precommit]
tr:293 [binder, in Giskard.precommit]
tr:297 [binder, in Giskard.precommit]
tr:30 [binder, in Giskard.prepare]
tr:303 [binder, in Giskard.precommit]
tr:308 [binder, in Giskard.precommit]
tr:312 [binder, in Giskard.precommit]
tr:317 [binder, in Giskard.precommit]
tr:322 [binder, in Giskard.precommit]
tr:327 [binder, in Giskard.precommit]
tr:33 [binder, in Giskard.precommit]
tr:332 [binder, in Giskard.precommit]
tr:340 [binder, in Giskard.precommit]
tr:348 [binder, in Giskard.precommit]
tr:35 [binder, in Giskard.prepare]
tr:353 [binder, in Giskard.precommit]
tr:358 [binder, in Giskard.precommit]
tr:36 [binder, in Giskard.global]
tr:363 [binder, in Giskard.precommit]
tr:369 [binder, in Giskard.precommit]
tr:37 [binder, in Giskard.precommit]
tr:37 [binder, in Giskard.global]
tr:374 [binder, in Giskard.precommit]
tr:38 [binder, in Giskard.global]
tr:38 [binder, in Giskard.prepare]
tr:380 [binder, in Giskard.precommit]
tr:386 [binder, in Giskard.precommit]
tr:392 [binder, in Giskard.precommit]
tr:40 [binder, in Giskard.global]
tr:42 [binder, in Giskard.precommit]
tr:43 [binder, in Giskard.global]
tr:45 [binder, in Giskard.prepare]
tr:46 [binder, in Giskard.precommit]
tr:47 [binder, in Giskard.global]
tr:48 [binder, in Giskard.prepare]
tr:51 [binder, in Giskard.precommit]
tr:55 [binder, in Giskard.global]
tr:56 [binder, in Giskard.precommit]
tr:59 [binder, in Giskard.global]
tr:6 [binder, in Giskard.commit]
tr:6 [binder, in Giskard.precommit]
tr:60 [binder, in Giskard.precommit]
tr:61 [binder, in Giskard.prepare]
tr:64 [binder, in Giskard.global]
tr:65 [binder, in Giskard.precommit]
tr:66 [binder, in Giskard.prepare]
tr:69 [binder, in Giskard.precommit]
tr:70 [binder, in Giskard.prepare]
tr:72 [binder, in Giskard.global]
tr:73 [binder, in Giskard.prepare]
tr:75 [binder, in Giskard.precommit]
tr:75 [binder, in Giskard.global]
tr:79 [binder, in Giskard.global]
tr:82 [binder, in Giskard.precommit]
tr:84 [binder, in Giskard.global]
tr:87 [binder, in Giskard.precommit]
tr:88 [binder, in Giskard.global]
tr:93 [binder, in Giskard.precommit]
tr:95 [binder, in Giskard.global]
t:153 [binder, in Giskard.local]
t:156 [binder, in Giskard.local]
t:194 [binder, in Giskard.local]
t:200 [binder, in Giskard.local]
t:206 [binder, in Giskard.local]
t:212 [binder, in Giskard.local]
t:31 [binder, in Giskard.global]
t:34 [binder, in Giskard.global]
V
ViewChange [constructor, in Giskard.structures]ViewChangeQC [constructor, in Giskard.structures]
ViewChange_message_block_prepare_stage_global [lemma, in Giskard.precommit]
ViewChange_quorum_global [lemma, in Giskard.global]
view_increment_exists_trigger_message_global [lemma, in Giskard.precommit]
view_same_or_plus_one [lemma, in Giskard.global]
view_different_tells_receiver [lemma, in Giskard.global]
view_state_morphism [lemma, in Giskard.global]
view_state_morphism_inductive_step [lemma, in Giskard.global]
view_change_quorum_in_view [definition, in Giskard.local]
view_validb [definition, in Giskard.local]
view_valid [definition, in Giskard.local]
view:46 [binder, in Giskard.local]
view:50 [binder, in Giskard.local]
view:53 [binder, in Giskard.local]
view:57 [binder, in Giskard.local]
view:60 [binder, in Giskard.local]
view:67 [binder, in Giskard.local]
view:70 [binder, in Giskard.local]
view:73 [binder, in Giskard.local]
view:75 [binder, in Giskard.local]
view:77 [binder, in Giskard.local]
view:80 [binder, in Giskard.local]
vote_quorum_in_view_global [definition, in Giskard.precommit]
vote_quorum_in_view_step_global [lemma, in Giskard.global]
vote_quorum_local_means_vote_quorum_global [lemma, in Giskard.global]
vote_quorum_in_view_global_step [lemma, in Giskard.global]
vote_quorum_in_view_persistent [lemma, in Giskard.global]
vote_quorum_in_view_global [definition, in Giskard.global]
vote_quorum_current_view_persistent [lemma, in Giskard.global]
vote_quorum_in_view [definition, in Giskard.local]
vote_quorum_in_view_step_global [lemma, in Giskard.prepare]
vote_quorum_local_means_vote_quorum_global [lemma, in Giskard.prepare]
vote_quorum_same_view_global_injective [lemma, in Giskard.prepare]
v_past:196 [binder, in Giskard.precommit]
v_past:177 [binder, in Giskard.global]
v':148 [binder, in Giskard.precommit]
v':367 [binder, in Giskard.precommit]
v':65 [binder, in Giskard.local]
v':81 [binder, in Giskard.precommit]
v1:110 [binder, in Giskard.structures]
v1:147 [binder, in Giskard.precommit]
v1:153 [binder, in Giskard.precommit]
v1:159 [binder, in Giskard.precommit]
v1:371 [binder, in Giskard.precommit]
v1:376 [binder, in Giskard.precommit]
v2:111 [binder, in Giskard.structures]
v2:154 [binder, in Giskard.precommit]
v2:160 [binder, in Giskard.precommit]
v2:377 [binder, in Giskard.precommit]
v:164 [binder, in Giskard.precommit]
v:267 [binder, in Giskard.precommit]
v:360 [binder, in Giskard.precommit]
v:365 [binder, in Giskard.precommit]
v:80 [binder, in Giskard.precommit]
W
wedged_in_between [lemma, in Giskard.global]witnessed_quorum_global [lemma, in Giskard.prepare]
X
x1:6 [binder, in Giskard.lib]x2:7 [binder, in Giskard.lib]
x:173 [binder, in Giskard.global]
x:2 [binder, in Giskard.lib]
x:228 [binder, in Giskard.precommit]
x:54 [binder, in Giskard.precommit]
Y
y:3 [binder, in Giskard.lib]Binder Index
A
A:1 [in Giskard.lib]B
b_child:5 [in Giskard.commit]b_child:166 [in Giskard.precommit]
b_child:86 [in Giskard.precommit]
b_child:79 [in Giskard.precommit]
b_child:5 [in Giskard.precommit]
b':112 [in Giskard.precommit]
b':143 [in Giskard.precommit]
b1:10 [in Giskard.commit]
b1:113 [in Giskard.structures]
b1:12 [in Giskard.structures]
b1:146 [in Giskard.precommit]
b1:151 [in Giskard.precommit]
b1:157 [in Giskard.precommit]
b1:160 [in Giskard.global]
b1:171 [in Giskard.precommit]
b1:22 [in Giskard.structures]
b1:253 [in Giskard.global]
b1:384 [in Giskard.precommit]
b1:390 [in Giskard.precommit]
b1:396 [in Giskard.precommit]
b1:5 [in Giskard.prepare]
b1:50 [in Giskard.prepare]
b1:64 [in Giskard.prepare]
b1:73 [in Giskard.precommit]
b1:76 [in Giskard.prepare]
b1:9 [in Giskard.structures]
b1:91 [in Giskard.precommit]
b2:10 [in Giskard.structures]
b2:11 [in Giskard.commit]
b2:114 [in Giskard.structures]
b2:13 [in Giskard.structures]
b2:152 [in Giskard.precommit]
b2:158 [in Giskard.precommit]
b2:172 [in Giskard.precommit]
b2:23 [in Giskard.structures]
b2:385 [in Giskard.precommit]
b2:391 [in Giskard.precommit]
b2:397 [in Giskard.precommit]
b2:51 [in Giskard.prepare]
b2:6 [in Giskard.prepare]
b2:74 [in Giskard.precommit]
b2:92 [in Giskard.precommit]
b:104 [in Giskard.precommit]
b:105 [in Giskard.precommit]
b:111 [in Giskard.precommit]
b:116 [in Giskard.precommit]
b:127 [in Giskard.precommit]
b:129 [in Giskard.precommit]
b:13 [in Giskard.precommit]
b:135 [in Giskard.precommit]
b:136 [in Giskard.precommit]
b:142 [in Giskard.precommit]
b:16 [in Giskard.structures]
b:165 [in Giskard.precommit]
b:17 [in Giskard.precommit]
b:18 [in Giskard.structures]
b:207 [in Giskard.global]
b:21 [in Giskard.precommit]
b:215 [in Giskard.global]
b:220 [in Giskard.global]
b:221 [in Giskard.local]
b:224 [in Giskard.precommit]
b:224 [in Giskard.global]
b:224 [in Giskard.local]
b:227 [in Giskard.precommit]
b:227 [in Giskard.local]
b:229 [in Giskard.global]
b:230 [in Giskard.local]
b:238 [in Giskard.global]
b:25 [in Giskard.structures]
b:257 [in Giskard.global]
b:26 [in Giskard.precommit]
b:26 [in Giskard.local]
b:260 [in Giskard.precommit]
b:262 [in Giskard.global]
b:269 [in Giskard.global]
b:27 [in Giskard.structures]
b:277 [in Giskard.precommit]
b:277 [in Giskard.global]
b:281 [in Giskard.global]
b:29 [in Giskard.structures]
b:30 [in Giskard.precommit]
b:30 [in Giskard.local]
b:33 [in Giskard.local]
b:331 [in Giskard.precommit]
b:35 [in Giskard.precommit]
b:35 [in Giskard.local]
b:37 [in Giskard.local]
b:4 [in Giskard.commit]
b:4 [in Giskard.precommit]
b:40 [in Giskard.precommit]
b:40 [in Giskard.local]
b:42 [in Giskard.local]
b:44 [in Giskard.precommit]
b:44 [in Giskard.local]
b:47 [in Giskard.local]
b:49 [in Giskard.precommit]
b:5 [in Giskard.structures]
b:51 [in Giskard.local]
b:53 [in Giskard.precommit]
b:54 [in Giskard.local]
b:58 [in Giskard.precommit]
b:58 [in Giskard.local]
b:61 [in Giskard.local]
b:63 [in Giskard.precommit]
b:64 [in Giskard.local]
b:68 [in Giskard.precommit]
b:68 [in Giskard.prepare]
b:7 [in Giskard.structures]
b:78 [in Giskard.precommit]
b:78 [in Giskard.local]
b:8 [in Giskard.precommit]
b:85 [in Giskard.precommit]
b:96 [in Giskard.precommit]
b:98 [in Giskard.precommit]
E
eq_dec:4 [in Giskard.lib]G
g':14 [in Giskard.global]g':16 [in Giskard.global]
g':19 [in Giskard.global]
g':26 [in Giskard.global]
g':30 [in Giskard.global]
g:13 [in Giskard.global]
g:15 [in Giskard.global]
g:18 [in Giskard.global]
g:2 [in Giskard.global]
g:25 [in Giskard.global]
g:27 [in Giskard.global]
g:29 [in Giskard.global]
g:33 [in Giskard.global]
H
highest_msg:104 [in Giskard.local]h_max:357 [in Giskard.precommit]
h_max:352 [in Giskard.precommit]
h_max:326 [in Giskard.precommit]
h_max:292 [in Giskard.precommit]
h_max:287 [in Giskard.precommit]
h_max:282 [in Giskard.precommit]
H_prot:264 [in Giskard.precommit]
h_local:123 [in Giskard.precommit]
h:102 [in Giskard.precommit]
h:109 [in Giskard.precommit]
h:117 [in Giskard.precommit]
h:120 [in Giskard.precommit]
h:126 [in Giskard.precommit]
h:133 [in Giskard.precommit]
h:140 [in Giskard.precommit]
h:329 [in Giskard.precommit]
h:342 [in Giskard.precommit]
h:95 [in Giskard.precommit]
I
i_past:178 [in Giskard.global]i_past:110 [in Giskard.global]
i1:180 [in Giskard.global]
i1:44 [in Giskard.global]
i2:181 [in Giskard.global]
i2:45 [in Giskard.global]
i:101 [in Giskard.precommit]
i:103 [in Giskard.global]
i:107 [in Giskard.precommit]
i:107 [in Giskard.global]
i:11 [in Giskard.precommit]
i:112 [in Giskard.global]
i:114 [in Giskard.precommit]
i:116 [in Giskard.global]
i:119 [in Giskard.precommit]
i:120 [in Giskard.global]
i:125 [in Giskard.precommit]
i:127 [in Giskard.global]
i:13 [in Giskard.prepare]
i:132 [in Giskard.precommit]
i:135 [in Giskard.global]
i:138 [in Giskard.precommit]
i:142 [in Giskard.global]
i:145 [in Giskard.precommit]
i:15 [in Giskard.precommit]
i:150 [in Giskard.precommit]
i:153 [in Giskard.global]
i:156 [in Giskard.precommit]
i:157 [in Giskard.global]
i:162 [in Giskard.precommit]
i:162 [in Giskard.global]
i:165 [in Giskard.global]
i:168 [in Giskard.precommit]
i:170 [in Giskard.global]
i:174 [in Giskard.precommit]
i:175 [in Giskard.global]
i:178 [in Giskard.precommit]
i:182 [in Giskard.precommit]
i:184 [in Giskard.global]
i:186 [in Giskard.precommit]
i:188 [in Giskard.global]
i:191 [in Giskard.precommit]
i:193 [in Giskard.global]
i:195 [in Giskard.precommit]
i:197 [in Giskard.global]
i:199 [in Giskard.precommit]
i:2 [in Giskard.commit]
i:2 [in Giskard.precommit]
i:2 [in Giskard.prepare]
i:20 [in Giskard.precommit]
i:201 [in Giskard.global]
i:206 [in Giskard.global]
i:208 [in Giskard.precommit]
i:21 [in Giskard.prepare]
i:212 [in Giskard.precommit]
i:214 [in Giskard.global]
i:216 [in Giskard.precommit]
i:219 [in Giskard.global]
i:220 [in Giskard.precommit]
i:223 [in Giskard.global]
i:226 [in Giskard.precommit]
i:228 [in Giskard.global]
i:231 [in Giskard.precommit]
i:236 [in Giskard.precommit]
i:237 [in Giskard.global]
i:24 [in Giskard.prepare]
i:240 [in Giskard.precommit]
i:245 [in Giskard.precommit]
i:248 [in Giskard.global]
i:25 [in Giskard.precommit]
i:251 [in Giskard.precommit]
i:251 [in Giskard.global]
i:255 [in Giskard.precommit]
i:256 [in Giskard.global]
i:259 [in Giskard.precommit]
i:261 [in Giskard.global]
i:265 [in Giskard.precommit]
i:268 [in Giskard.global]
i:27 [in Giskard.prepare]
i:270 [in Giskard.precommit]
i:273 [in Giskard.precommit]
i:276 [in Giskard.global]
i:279 [in Giskard.precommit]
i:284 [in Giskard.precommit]
i:289 [in Giskard.precommit]
i:29 [in Giskard.precommit]
i:295 [in Giskard.precommit]
i:299 [in Giskard.precommit]
i:304 [in Giskard.precommit]
i:309 [in Giskard.precommit]
i:313 [in Giskard.precommit]
i:318 [in Giskard.precommit]
i:32 [in Giskard.prepare]
i:323 [in Giskard.precommit]
i:328 [in Giskard.precommit]
i:333 [in Giskard.precommit]
i:34 [in Giskard.precommit]
i:341 [in Giskard.precommit]
i:349 [in Giskard.precommit]
i:354 [in Giskard.precommit]
i:359 [in Giskard.precommit]
i:364 [in Giskard.precommit]
i:37 [in Giskard.prepare]
i:381 [in Giskard.precommit]
i:387 [in Giskard.precommit]
i:39 [in Giskard.precommit]
i:393 [in Giskard.precommit]
i:40 [in Giskard.prepare]
i:41 [in Giskard.global]
i:43 [in Giskard.precommit]
i:47 [in Giskard.precommit]
i:47 [in Giskard.prepare]
i:48 [in Giskard.global]
i:49 [in Giskard.prepare]
i:52 [in Giskard.precommit]
i:56 [in Giskard.global]
i:57 [in Giskard.precommit]
i:61 [in Giskard.precommit]
i:62 [in Giskard.prepare]
i:65 [in Giskard.global]
i:66 [in Giskard.precommit]
i:67 [in Giskard.prepare]
i:7 [in Giskard.commit]
i:7 [in Giskard.precommit]
i:70 [in Giskard.precommit]
i:71 [in Giskard.prepare]
i:74 [in Giskard.prepare]
i:76 [in Giskard.precommit]
i:80 [in Giskard.global]
i:83 [in Giskard.precommit]
i:85 [in Giskard.global]
i:88 [in Giskard.precommit]
i:89 [in Giskard.global]
i:94 [in Giskard.precommit]
i:96 [in Giskard.global]
J
j:166 [in Giskard.global]j:171 [in Giskard.global]
j:208 [in Giskard.global]
j:231 [in Giskard.global]
j:264 [in Giskard.global]
j:272 [in Giskard.global]
j:279 [in Giskard.global]
j:370 [in Giskard.precommit]
j:375 [in Giskard.precommit]
j:41 [in Giskard.precommit]
j:48 [in Giskard.precommit]
L
lm0:101 [in Giskard.global]lm0:123 [in Giskard.global]
lm0:131 [in Giskard.global]
lm0:138 [in Giskard.global]
lm0:206 [in Giskard.precommit]
lm0:52 [in Giskard.global]
lm0:69 [in Giskard.global]
lm0:83 [in Giskard.global]
lm0:94 [in Giskard.global]
lm1:119 [in Giskard.structures]
lm2:120 [in Giskard.structures]
lm:109 [in Giskard.local]
lm:113 [in Giskard.local]
lm:117 [in Giskard.structures]
lm:117 [in Giskard.local]
lm:118 [in Giskard.structures]
lm:12 [in Giskard.global]
lm:12 [in Giskard.local]
lm:121 [in Giskard.local]
lm:123 [in Giskard.structures]
lm:125 [in Giskard.local]
lm:129 [in Giskard.local]
lm:133 [in Giskard.local]
lm:137 [in Giskard.local]
lm:141 [in Giskard.local]
lm:145 [in Giskard.local]
lm:149 [in Giskard.local]
lm:154 [in Giskard.local]
lm:157 [in Giskard.local]
lm:174 [in Giskard.local]
lm:178 [in Giskard.local]
lm:182 [in Giskard.local]
lm:187 [in Giskard.local]
lm:191 [in Giskard.local]
lm:199 [in Giskard.local]
lm:205 [in Giskard.local]
lm:211 [in Giskard.local]
lm:217 [in Giskard.local]
lm:228 [in Giskard.local]
lm:23 [in Giskard.global]
lm:231 [in Giskard.local]
lm:336 [in Giskard.precommit]
lm:344 [in Giskard.precommit]
lm:5 [in Giskard.global]
lm:8 [in Giskard.local]
ln:73 [in Giskard.structures]
l_superset:60 [in Giskard.structures]
l1:65 [in Giskard.structures]
l2:66 [in Giskard.structures]
l:47 [in Giskard.structures]
l:49 [in Giskard.structures]
l:5 [in Giskard.lib]
l:50 [in Giskard.structures]
l:53 [in Giskard.structures]
l:56 [in Giskard.structures]
l:59 [in Giskard.structures]
l:64 [in Giskard.structures]
l:67 [in Giskard.structures]
M
msg':15 [in Giskard.prepare]msg':203 [in Giskard.global]
msg':302 [in Giskard.precommit]
msg':316 [in Giskard.precommit]
msg':321 [in Giskard.precommit]
msg':362 [in Giskard.precommit]
msg':368 [in Giskard.precommit]
msg0:100 [in Giskard.global]
msg0:125 [in Giskard.global]
msg0:130 [in Giskard.global]
msg0:140 [in Giskard.global]
msg0:201 [in Giskard.local]
msg0:205 [in Giskard.precommit]
msg0:207 [in Giskard.local]
msg0:213 [in Giskard.local]
msg0:219 [in Giskard.local]
msg0:245 [in Giskard.global]
msg0:346 [in Giskard.precommit]
msg0:51 [in Giskard.global]
msg0:68 [in Giskard.global]
msg0:88 [in Giskard.local]
msg0:93 [in Giskard.global]
msg0:98 [in Giskard.local]
msg1:115 [in Giskard.structures]
msg1:150 [in Giskard.local]
msg1:159 [in Giskard.global]
msg1:17 [in Giskard.prepare]
msg1:229 [in Giskard.precommit]
msg1:23 [in Giskard.local]
msg1:233 [in Giskard.precommit]
msg1:237 [in Giskard.precommit]
msg1:242 [in Giskard.precommit]
msg1:247 [in Giskard.precommit]
msg1:252 [in Giskard.precommit]
msg1:256 [in Giskard.precommit]
msg1:28 [in Giskard.prepare]
msg1:33 [in Giskard.prepare]
msg1:372 [in Giskard.precommit]
msg1:378 [in Giskard.precommit]
msg1:43 [in Giskard.prepare]
msg1:55 [in Giskard.precommit]
msg1:9 [in Giskard.prepare]
msg2:10 [in Giskard.prepare]
msg2:116 [in Giskard.structures]
msg2:151 [in Giskard.local]
msg2:18 [in Giskard.prepare]
msg2:234 [in Giskard.precommit]
msg2:238 [in Giskard.precommit]
msg2:24 [in Giskard.local]
msg2:243 [in Giskard.precommit]
msg2:249 [in Giskard.precommit]
msg2:253 [in Giskard.precommit]
msg2:257 [in Giskard.precommit]
msg2:29 [in Giskard.prepare]
msg2:34 [in Giskard.prepare]
msg2:373 [in Giskard.precommit]
msg2:379 [in Giskard.precommit]
msg2:44 [in Giskard.prepare]
msg:101 [in Giskard.local]
msg:105 [in Giskard.global]
msg:107 [in Giskard.local]
msg:109 [in Giskard.global]
msg:11 [in Giskard.global]
msg:111 [in Giskard.local]
msg:114 [in Giskard.global]
msg:115 [in Giskard.local]
msg:118 [in Giskard.global]
msg:119 [in Giskard.local]
msg:121 [in Giskard.global]
msg:121 [in Giskard.structures]
msg:123 [in Giskard.local]
msg:124 [in Giskard.structures]
msg:127 [in Giskard.local]
msg:131 [in Giskard.local]
msg:133 [in Giskard.global]
msg:135 [in Giskard.local]
msg:136 [in Giskard.global]
msg:139 [in Giskard.local]
msg:14 [in Giskard.prepare]
msg:143 [in Giskard.global]
msg:143 [in Giskard.local]
msg:145 [in Giskard.global]
msg:146 [in Giskard.global]
msg:147 [in Giskard.global]
msg:147 [in Giskard.local]
msg:148 [in Giskard.global]
msg:149 [in Giskard.global]
msg:150 [in Giskard.global]
msg:151 [in Giskard.global]
msg:154 [in Giskard.global]
msg:158 [in Giskard.local]
msg:16 [in Giskard.local]
msg:161 [in Giskard.local]
msg:162 [in Giskard.local]
msg:164 [in Giskard.local]
msg:165 [in Giskard.local]
msg:166 [in Giskard.local]
msg:168 [in Giskard.global]
msg:168 [in Giskard.local]
msg:169 [in Giskard.local]
msg:170 [in Giskard.local]
msg:172 [in Giskard.local]
msg:176 [in Giskard.precommit]
msg:176 [in Giskard.local]
msg:180 [in Giskard.precommit]
msg:180 [in Giskard.local]
msg:184 [in Giskard.precommit]
msg:185 [in Giskard.global]
msg:185 [in Giskard.local]
msg:188 [in Giskard.precommit]
msg:189 [in Giskard.global]
msg:189 [in Giskard.local]
msg:19 [in Giskard.local]
msg:192 [in Giskard.precommit]
msg:194 [in Giskard.global]
msg:197 [in Giskard.precommit]
msg:198 [in Giskard.global]
msg:198 [in Giskard.local]
msg:202 [in Giskard.precommit]
msg:202 [in Giskard.global]
msg:204 [in Giskard.local]
msg:209 [in Giskard.global]
msg:21 [in Giskard.local]
msg:210 [in Giskard.precommit]
msg:210 [in Giskard.global]
msg:210 [in Giskard.local]
msg:211 [in Giskard.global]
msg:212 [in Giskard.global]
msg:214 [in Giskard.precommit]
msg:216 [in Giskard.local]
msg:217 [in Giskard.global]
msg:218 [in Giskard.precommit]
msg:22 [in Giskard.global]
msg:221 [in Giskard.global]
msg:222 [in Giskard.local]
msg:223 [in Giskard.precommit]
msg:225 [in Giskard.local]
msg:23 [in Giskard.precommit]
msg:232 [in Giskard.global]
msg:232 [in Giskard.local]
msg:233 [in Giskard.global]
msg:234 [in Giskard.global]
msg:235 [in Giskard.global]
msg:240 [in Giskard.global]
msg:241 [in Giskard.global]
msg:242 [in Giskard.global]
msg:243 [in Giskard.global]
msg:246 [in Giskard.global]
msg:249 [in Giskard.global]
msg:262 [in Giskard.precommit]
msg:263 [in Giskard.global]
msg:265 [in Giskard.global]
msg:266 [in Giskard.precommit]
msg:27 [in Giskard.local]
msg:271 [in Giskard.precommit]
msg:271 [in Giskard.global]
msg:273 [in Giskard.global]
msg:276 [in Giskard.precommit]
msg:28 [in Giskard.local]
msg:281 [in Giskard.precommit]
msg:286 [in Giskard.precommit]
msg:291 [in Giskard.precommit]
msg:296 [in Giskard.precommit]
msg:301 [in Giskard.precommit]
msg:307 [in Giskard.precommit]
msg:31 [in Giskard.local]
msg:311 [in Giskard.precommit]
msg:315 [in Giskard.precommit]
msg:32 [in Giskard.precommit]
msg:320 [in Giskard.precommit]
msg:325 [in Giskard.precommit]
msg:335 [in Giskard.precommit]
msg:337 [in Giskard.precommit]
msg:338 [in Giskard.precommit]
msg:34 [in Giskard.local]
msg:345 [in Giskard.precommit]
msg:351 [in Giskard.precommit]
msg:356 [in Giskard.precommit]
msg:36 [in Giskard.local]
msg:361 [in Giskard.precommit]
msg:366 [in Giskard.precommit]
msg:38 [in Giskard.local]
msg:48 [in Giskard.local]
msg:54 [in Giskard.global]
msg:55 [in Giskard.local]
msg:58 [in Giskard.global]
msg:62 [in Giskard.local]
msg:63 [in Giskard.global]
msg:68 [in Giskard.local]
msg:71 [in Giskard.global]
msg:71 [in Giskard.local]
msg:72 [in Giskard.prepare]
msg:74 [in Giskard.global]
msg:78 [in Giskard.global]
msg:83 [in Giskard.local]
msg:87 [in Giskard.global]
msg:89 [in Giskard.local]
msg:95 [in Giskard.local]
msg:99 [in Giskard.local]
mt1:79 [in Giskard.structures]
mt1:81 [in Giskard.structures]
mt1:83 [in Giskard.structures]
mt2:80 [in Giskard.structures]
mt2:82 [in Giskard.structures]
mt2:84 [in Giskard.structures]
m1:91 [in Giskard.structures]
m1:93 [in Giskard.structures]
m1:95 [in Giskard.structures]
m2:92 [in Giskard.structures]
m2:94 [in Giskard.structures]
m2:96 [in Giskard.structures]
m:10 [in Giskard.local]
m:11 [in Giskard.lib]
m:14 [in Giskard.local]
m:170 [in Giskard.precommit]
m:2 [in Giskard.local]
m:383 [in Giskard.precommit]
m:389 [in Giskard.precommit]
m:395 [in Giskard.precommit]
m:4 [in Giskard.local]
m:4 [in Giskard.prepare]
m:50 [in Giskard.global]
m:6 [in Giskard.local]
m:72 [in Giskard.precommit]
m:9 [in Giskard.commit]
m:90 [in Giskard.precommit]
m:92 [in Giskard.global]
m:99 [in Giskard.global]
N
ns:71 [in Giskard.structures]n':248 [in Giskard.precommit]
n0:122 [in Giskard.global]
n0:128 [in Giskard.global]
n0:137 [in Giskard.global]
n0:203 [in Giskard.precommit]
n0:66 [in Giskard.global]
n0:82 [in Giskard.global]
n1:108 [in Giskard.structures]
n1:32 [in Giskard.structures]
n1:36 [in Giskard.structures]
n1:38 [in Giskard.structures]
n1:40 [in Giskard.structures]
n1:60 [in Giskard.global]
n1:76 [in Giskard.global]
n2:109 [in Giskard.structures]
n2:33 [in Giskard.structures]
n2:37 [in Giskard.structures]
n2:39 [in Giskard.structures]
n2:41 [in Giskard.structures]
n2:61 [in Giskard.global]
n2:77 [in Giskard.global]
n:1 [in Giskard.global]
n:10 [in Giskard.lib]
n:104 [in Giskard.global]
n:104 [in Giskard.structures]
n:108 [in Giskard.precommit]
n:108 [in Giskard.global]
n:113 [in Giskard.global]
n:117 [in Giskard.global]
n:12 [in Giskard.precommit]
n:12 [in Giskard.prepare]
n:122 [in Giskard.precommit]
n:132 [in Giskard.global]
n:139 [in Giskard.precommit]
n:144 [in Giskard.global]
n:152 [in Giskard.local]
n:155 [in Giskard.global]
n:155 [in Giskard.local]
n:158 [in Giskard.global]
n:16 [in Giskard.precommit]
n:163 [in Giskard.precommit]
n:163 [in Giskard.global]
n:167 [in Giskard.global]
n:169 [in Giskard.precommit]
n:17 [in Giskard.global]
n:172 [in Giskard.global]
n:176 [in Giskard.global]
n:182 [in Giskard.global]
n:187 [in Giskard.global]
n:190 [in Giskard.precommit]
n:192 [in Giskard.global]
n:194 [in Giskard.precommit]
n:196 [in Giskard.global]
n:20 [in Giskard.global]
n:20 [in Giskard.prepare]
n:200 [in Giskard.global]
n:201 [in Giskard.precommit]
n:205 [in Giskard.global]
n:221 [in Giskard.precommit]
n:227 [in Giskard.global]
n:23 [in Giskard.prepare]
n:232 [in Giskard.precommit]
n:24 [in Giskard.global]
n:241 [in Giskard.precommit]
n:246 [in Giskard.precommit]
n:252 [in Giskard.global]
n:26 [in Giskard.prepare]
n:260 [in Giskard.global]
n:267 [in Giskard.global]
n:274 [in Giskard.precommit]
n:275 [in Giskard.global]
n:28 [in Giskard.global]
n:280 [in Giskard.global]
n:294 [in Giskard.precommit]
n:298 [in Giskard.precommit]
n:3 [in Giskard.commit]
n:3 [in Giskard.precommit]
n:3 [in Giskard.prepare]
n:306 [in Giskard.precommit]
n:31 [in Giskard.prepare]
n:32 [in Giskard.global]
n:339 [in Giskard.precommit]
n:347 [in Giskard.precommit]
n:35 [in Giskard.global]
n:35 [in Giskard.structures]
n:36 [in Giskard.prepare]
n:38 [in Giskard.precommit]
n:382 [in Giskard.precommit]
n:388 [in Giskard.precommit]
n:39 [in Giskard.global]
n:39 [in Giskard.prepare]
n:394 [in Giskard.precommit]
n:42 [in Giskard.global]
n:42 [in Giskard.prepare]
n:44 [in Giskard.structures]
n:46 [in Giskard.global]
n:46 [in Giskard.prepare]
n:51 [in Giskard.structures]
n:53 [in Giskard.global]
n:53 [in Giskard.prepare]
n:54 [in Giskard.structures]
n:54 [in Giskard.prepare]
n:55 [in Giskard.prepare]
n:56 [in Giskard.prepare]
n:57 [in Giskard.global]
n:57 [in Giskard.structures]
n:57 [in Giskard.prepare]
n:58 [in Giskard.prepare]
n:59 [in Giskard.prepare]
n:6 [in Giskard.global]
n:60 [in Giskard.prepare]
n:61 [in Giskard.structures]
n:62 [in Giskard.precommit]
n:62 [in Giskard.global]
n:63 [in Giskard.structures]
n:63 [in Giskard.prepare]
n:67 [in Giskard.precommit]
n:68 [in Giskard.structures]
n:70 [in Giskard.global]
n:70 [in Giskard.structures]
n:71 [in Giskard.precommit]
n:72 [in Giskard.structures]
n:73 [in Giskard.global]
n:75 [in Giskard.structures]
n:75 [in Giskard.prepare]
n:77 [in Giskard.precommit]
n:8 [in Giskard.commit]
n:81 [in Giskard.global]
n:84 [in Giskard.precommit]
n:86 [in Giskard.global]
n:89 [in Giskard.precommit]
n:9 [in Giskard.precommit]
n:9 [in Giskard.global]
n:90 [in Giskard.global]
n:97 [in Giskard.global]
P
pb_msg:268 [in Giskard.precommit]prepareblock_msg:92 [in Giskard.local]
prepare_block_msg:96 [in Giskard.local]
previous_msg:86 [in Giskard.local]
process:10 [in Giskard.global]
process:21 [in Giskard.global]
p0:124 [in Giskard.global]
p0:129 [in Giskard.global]
p0:139 [in Giskard.global]
p0:204 [in Giskard.precommit]
p0:49 [in Giskard.global]
p0:67 [in Giskard.global]
p0:91 [in Giskard.global]
p0:98 [in Giskard.global]
p:103 [in Giskard.precommit]
p:110 [in Giskard.precommit]
p:115 [in Giskard.precommit]
p:121 [in Giskard.precommit]
p:128 [in Giskard.precommit]
p:130 [in Giskard.precommit]
p:134 [in Giskard.precommit]
p:141 [in Giskard.precommit]
p:175 [in Giskard.precommit]
p:179 [in Giskard.precommit]
p:18 [in Giskard.precommit]
p:183 [in Giskard.precommit]
p:187 [in Giskard.precommit]
P:190 [in Giskard.global]
p:200 [in Giskard.precommit]
p:209 [in Giskard.precommit]
p:213 [in Giskard.precommit]
p:216 [in Giskard.global]
p:217 [in Giskard.precommit]
p:218 [in Giskard.local]
p:22 [in Giskard.precommit]
p:222 [in Giskard.precommit]
p:225 [in Giskard.global]
p:230 [in Giskard.global]
p:239 [in Giskard.global]
p:254 [in Giskard.global]
p:258 [in Giskard.global]
p:261 [in Giskard.precommit]
p:27 [in Giskard.precommit]
p:270 [in Giskard.global]
p:275 [in Giskard.precommit]
p:278 [in Giskard.global]
p:280 [in Giskard.precommit]
p:285 [in Giskard.precommit]
p:290 [in Giskard.precommit]
p:300 [in Giskard.precommit]
p:305 [in Giskard.precommit]
p:31 [in Giskard.precommit]
p:310 [in Giskard.precommit]
p:314 [in Giskard.precommit]
p:319 [in Giskard.precommit]
p:324 [in Giskard.precommit]
p:330 [in Giskard.precommit]
p:334 [in Giskard.precommit]
p:343 [in Giskard.precommit]
p:350 [in Giskard.precommit]
p:355 [in Giskard.precommit]
p:36 [in Giskard.precommit]
p:45 [in Giskard.precommit]
p:50 [in Giskard.precommit]
p:52 [in Giskard.prepare]
p:59 [in Giskard.precommit]
p:64 [in Giskard.precommit]
p:65 [in Giskard.prepare]
p:69 [in Giskard.prepare]
p:7 [in Giskard.prepare]
p:77 [in Giskard.prepare]
P:8 [in Giskard.lib]
p:97 [in Giskard.precommit]
p:99 [in Giskard.precommit]
Q
quorum_msg:94 [in Giskard.local]quorum_msg:91 [in Giskard.local]
Q:9 [in Giskard.lib]
S
s':108 [in Giskard.local]s':112 [in Giskard.local]
s':116 [in Giskard.local]
s':120 [in Giskard.local]
s':124 [in Giskard.local]
s':128 [in Giskard.local]
s':132 [in Giskard.local]
s':136 [in Giskard.local]
s':140 [in Giskard.local]
s':144 [in Giskard.local]
s':148 [in Giskard.local]
s':173 [in Giskard.local]
s':177 [in Giskard.local]
s':181 [in Giskard.local]
s':186 [in Giskard.local]
s':190 [in Giskard.local]
s1:105 [in Giskard.structures]
s1:196 [in Giskard.local]
s1:202 [in Giskard.local]
s1:208 [in Giskard.local]
s1:214 [in Giskard.local]
s1:3 [in Giskard.global]
s2:106 [in Giskard.structures]
s2:197 [in Giskard.local]
s2:203 [in Giskard.local]
s2:209 [in Giskard.local]
s2:215 [in Giskard.local]
s2:4 [in Giskard.global]
s:1 [in Giskard.local]
s:100 [in Giskard.local]
s:102 [in Giskard.local]
s:103 [in Giskard.local]
s:105 [in Giskard.local]
s:106 [in Giskard.local]
s:11 [in Giskard.local]
s:110 [in Giskard.local]
s:114 [in Giskard.local]
s:118 [in Giskard.local]
s:122 [in Giskard.local]
s:126 [in Giskard.local]
s:13 [in Giskard.local]
s:130 [in Giskard.local]
s:134 [in Giskard.local]
s:138 [in Giskard.local]
s:142 [in Giskard.local]
s:146 [in Giskard.local]
s:15 [in Giskard.local]
s:159 [in Giskard.local]
s:16 [in Giskard.prepare]
s:160 [in Giskard.local]
s:163 [in Giskard.local]
s:167 [in Giskard.local]
s:17 [in Giskard.local]
s:171 [in Giskard.local]
s:175 [in Giskard.local]
s:179 [in Giskard.local]
s:18 [in Giskard.local]
s:183 [in Giskard.local]
s:184 [in Giskard.local]
s:188 [in Giskard.local]
s:20 [in Giskard.local]
s:22 [in Giskard.local]
s:220 [in Giskard.local]
s:223 [in Giskard.local]
s:226 [in Giskard.local]
s:229 [in Giskard.local]
s:244 [in Giskard.global]
s:25 [in Giskard.local]
s:29 [in Giskard.local]
s:3 [in Giskard.local]
s:32 [in Giskard.local]
s:39 [in Giskard.local]
s:41 [in Giskard.local]
s:41 [in Giskard.prepare]
s:43 [in Giskard.local]
s:45 [in Giskard.local]
s:49 [in Giskard.local]
s:5 [in Giskard.local]
s:52 [in Giskard.local]
s:56 [in Giskard.local]
s:59 [in Giskard.local]
s:63 [in Giskard.local]
s:66 [in Giskard.local]
s:69 [in Giskard.local]
s:7 [in Giskard.local]
s:72 [in Giskard.local]
s:74 [in Giskard.local]
s:76 [in Giskard.local]
s:79 [in Giskard.local]
s:8 [in Giskard.prepare]
s:84 [in Giskard.local]
s:85 [in Giskard.local]
s:87 [in Giskard.local]
s:9 [in Giskard.local]
s:90 [in Giskard.local]
s:93 [in Giskard.local]
s:97 [in Giskard.local]
T
tr:1 [in Giskard.commit]tr:1 [in Giskard.precommit]
tr:1 [in Giskard.prepare]
tr:10 [in Giskard.precommit]
tr:100 [in Giskard.precommit]
tr:102 [in Giskard.global]
tr:106 [in Giskard.precommit]
tr:106 [in Giskard.global]
tr:11 [in Giskard.prepare]
tr:111 [in Giskard.global]
tr:113 [in Giskard.precommit]
tr:115 [in Giskard.global]
tr:118 [in Giskard.precommit]
tr:119 [in Giskard.global]
tr:124 [in Giskard.precommit]
tr:126 [in Giskard.global]
tr:131 [in Giskard.precommit]
tr:134 [in Giskard.global]
tr:137 [in Giskard.precommit]
tr:14 [in Giskard.precommit]
tr:141 [in Giskard.global]
tr:144 [in Giskard.precommit]
tr:149 [in Giskard.precommit]
tr:152 [in Giskard.global]
tr:155 [in Giskard.precommit]
tr:156 [in Giskard.global]
tr:161 [in Giskard.precommit]
tr:161 [in Giskard.global]
tr:164 [in Giskard.global]
tr:167 [in Giskard.precommit]
tr:169 [in Giskard.global]
tr:173 [in Giskard.precommit]
tr:174 [in Giskard.global]
tr:177 [in Giskard.precommit]
tr:179 [in Giskard.global]
tr:181 [in Giskard.precommit]
tr:183 [in Giskard.global]
tr:185 [in Giskard.precommit]
tr:186 [in Giskard.global]
tr:189 [in Giskard.precommit]
tr:19 [in Giskard.precommit]
tr:19 [in Giskard.prepare]
tr:191 [in Giskard.global]
tr:193 [in Giskard.precommit]
tr:195 [in Giskard.global]
tr:198 [in Giskard.precommit]
tr:199 [in Giskard.global]
tr:204 [in Giskard.global]
tr:207 [in Giskard.precommit]
tr:211 [in Giskard.precommit]
tr:213 [in Giskard.global]
tr:215 [in Giskard.precommit]
tr:218 [in Giskard.global]
tr:219 [in Giskard.precommit]
tr:22 [in Giskard.prepare]
tr:222 [in Giskard.global]
tr:225 [in Giskard.precommit]
tr:226 [in Giskard.global]
tr:230 [in Giskard.precommit]
tr:235 [in Giskard.precommit]
tr:236 [in Giskard.global]
tr:239 [in Giskard.precommit]
tr:24 [in Giskard.precommit]
tr:244 [in Giskard.precommit]
tr:247 [in Giskard.global]
tr:25 [in Giskard.prepare]
tr:250 [in Giskard.precommit]
tr:250 [in Giskard.global]
tr:254 [in Giskard.precommit]
tr:255 [in Giskard.global]
tr:258 [in Giskard.precommit]
tr:259 [in Giskard.global]
tr:263 [in Giskard.precommit]
tr:266 [in Giskard.global]
tr:269 [in Giskard.precommit]
tr:272 [in Giskard.precommit]
tr:274 [in Giskard.global]
tr:278 [in Giskard.precommit]
tr:28 [in Giskard.precommit]
tr:283 [in Giskard.precommit]
tr:288 [in Giskard.precommit]
tr:293 [in Giskard.precommit]
tr:297 [in Giskard.precommit]
tr:30 [in Giskard.prepare]
tr:303 [in Giskard.precommit]
tr:308 [in Giskard.precommit]
tr:312 [in Giskard.precommit]
tr:317 [in Giskard.precommit]
tr:322 [in Giskard.precommit]
tr:327 [in Giskard.precommit]
tr:33 [in Giskard.precommit]
tr:332 [in Giskard.precommit]
tr:340 [in Giskard.precommit]
tr:348 [in Giskard.precommit]
tr:35 [in Giskard.prepare]
tr:353 [in Giskard.precommit]
tr:358 [in Giskard.precommit]
tr:36 [in Giskard.global]
tr:363 [in Giskard.precommit]
tr:369 [in Giskard.precommit]
tr:37 [in Giskard.precommit]
tr:37 [in Giskard.global]
tr:374 [in Giskard.precommit]
tr:38 [in Giskard.global]
tr:38 [in Giskard.prepare]
tr:380 [in Giskard.precommit]
tr:386 [in Giskard.precommit]
tr:392 [in Giskard.precommit]
tr:40 [in Giskard.global]
tr:42 [in Giskard.precommit]
tr:43 [in Giskard.global]
tr:45 [in Giskard.prepare]
tr:46 [in Giskard.precommit]
tr:47 [in Giskard.global]
tr:48 [in Giskard.prepare]
tr:51 [in Giskard.precommit]
tr:55 [in Giskard.global]
tr:56 [in Giskard.precommit]
tr:59 [in Giskard.global]
tr:6 [in Giskard.commit]
tr:6 [in Giskard.precommit]
tr:60 [in Giskard.precommit]
tr:61 [in Giskard.prepare]
tr:64 [in Giskard.global]
tr:65 [in Giskard.precommit]
tr:66 [in Giskard.prepare]
tr:69 [in Giskard.precommit]
tr:70 [in Giskard.prepare]
tr:72 [in Giskard.global]
tr:73 [in Giskard.prepare]
tr:75 [in Giskard.precommit]
tr:75 [in Giskard.global]
tr:79 [in Giskard.global]
tr:82 [in Giskard.precommit]
tr:84 [in Giskard.global]
tr:87 [in Giskard.precommit]
tr:88 [in Giskard.global]
tr:93 [in Giskard.precommit]
tr:95 [in Giskard.global]
t:153 [in Giskard.local]
t:156 [in Giskard.local]
t:194 [in Giskard.local]
t:200 [in Giskard.local]
t:206 [in Giskard.local]
t:212 [in Giskard.local]
t:31 [in Giskard.global]
t:34 [in Giskard.global]
V
view:46 [in Giskard.local]view:50 [in Giskard.local]
view:53 [in Giskard.local]
view:57 [in Giskard.local]
view:60 [in Giskard.local]
view:67 [in Giskard.local]
view:70 [in Giskard.local]
view:73 [in Giskard.local]
view:75 [in Giskard.local]
view:77 [in Giskard.local]
view:80 [in Giskard.local]
v_past:196 [in Giskard.precommit]
v_past:177 [in Giskard.global]
v':148 [in Giskard.precommit]
v':367 [in Giskard.precommit]
v':65 [in Giskard.local]
v':81 [in Giskard.precommit]
v1:110 [in Giskard.structures]
v1:147 [in Giskard.precommit]
v1:153 [in Giskard.precommit]
v1:159 [in Giskard.precommit]
v1:371 [in Giskard.precommit]
v1:376 [in Giskard.precommit]
v2:111 [in Giskard.structures]
v2:154 [in Giskard.precommit]
v2:160 [in Giskard.precommit]
v2:377 [in Giskard.precommit]
v:164 [in Giskard.precommit]
v:267 [in Giskard.precommit]
v:360 [in Giskard.precommit]
v:365 [in Giskard.precommit]
v:80 [in Giskard.precommit]
X
x1:6 [in Giskard.lib]x2:7 [in Giskard.lib]
x:173 [in Giskard.global]
x:2 [in Giskard.lib]
x:228 [in Giskard.precommit]
x:54 [in Giskard.precommit]
Y
y:3 [in Giskard.lib]Library Index
C
commitG
globalL
liblocal
P
precommitprepare
S
structuresLemma Index
A
about_generate_new_block [in Giskard.structures]about_local_out_messages [in Giskard.local]
about_highest_message_in_list [in Giskard.local]
C
commit_height_injective [in Giskard.commit]counting_messages_inclusion [in Giskard.global]
counting_message_change_view_change [in Giskard.global]
counting_message_different_tells_receiver [in Giskard.global]
counting_messages_monotonic [in Giskard.global]
counting_messages_change_tells_receiver [in Giskard.global]
counting_messages_local_monotonic [in Giskard.local]
counting_messages_same_view_monotonic [in Giskard.local]
D
delivered_means_sender_made_transition [in Giskard.global]delivered_means_sent_local [in Giskard.global]
delivered_means_sent_global [in Giskard.global]
E
empty_has_no_one_third [in Giskard.structures]empty_has_no_two_thirds [in Giskard.structures]
exists_same_height_block_correct [in Giskard.local]
G
get_view_highest_ViewChange_message_in_counting_messages [in Giskard.local]get_view_highest_ViewChange_message_node_view [in Giskard.local]
global_local_out_if [in Giskard.global]
global_messages_monotonic [in Giskard.global]
global_messages_monotonic_step [in Giskard.global]
global_equivocating_local [in Giskard.prepare]
GState_init_protocol_state [in Giskard.global]
GState_sane_transition [in Giskard.global]
GState_init_sane [in Giskard.global]
GState_step_transition [in Giskard.global]
H
highest_ViewChange_message_type_eq_ViewChange [in Giskard.local]I
is_max_prepare_height_in_view_disj_global [in Giskard.precommit]is_member_correct [in Giskard.structures]
L
last_block_highest_block_global [in Giskard.precommit]last_block_highest_block_sent [in Giskard.precommit]
le_S_disj [in Giskard.lib]
lift_sent_to_received [in Giskard.global]
local_leq_global [in Giskard.precommit]
local_global_out_if [in Giskard.global]
local_evidence_of_equivocation [in Giskard.prepare]
M
majority_shrink [in Giskard.structures]make_PrepareBlocks_message_type [in Giskard.global]
make_PrepareBlocks_message_type [in Giskard.local]
message_type_PrepareVote [in Giskard.global]
message_eqb_correct [in Giskard.structures]
message_type_eqb_correct [in Giskard.structures]
modus_tollens [in Giskard.lib]
N
node_eqb_no [in Giskard.structures]node_eqb_comm [in Giskard.structures]
node_eqb_refl [in Giskard.structures]
normal_trigger_message_highest_global [in Giskard.precommit]
not_my_problem [in Giskard.global]
not_prepare_stage [in Giskard.local]
no_prepare_blocks_GState_init [in Giskard.global]
O
out_message_view_bound [in Giskard.precommit]out_message_change_tells_sender [in Giskard.global]
out_messages_change_means_sent [in Giskard.global]
out_messages_global_monotonic [in Giskard.global]
out_messages_global_monotonic_step [in Giskard.global]
out_messages_local_monotonic [in Giskard.local]
P
participation_rights [in Giskard.global]participation_rights_global [in Giskard.global]
past_view_trigger_message_lowest_block_global [in Giskard.precommit]
past_view_exists_trigger_message_global [in Giskard.precommit]
pending_PrepareVote_correct [in Giskard.local]
precommit_now_height_injective [in Giskard.precommit]
precommit_now_height_injective_symmetric [in Giskard.precommit]
precommit_height_injective_symmetric [in Giskard.precommit]
precommit_stage_means_prepare_stage_global [in Giskard.precommit]
precommit_means_prepare [in Giskard.precommit]
PrepareBlock_sender_view_injective_global [in Giskard.precommit]
PrepareBlock_sender_is_new_proposer_global [in Giskard.precommit]
PrepareBlock_sender_is_new_proposer_local [in Giskard.precommit]
PrepareBlock_block_height_geq [in Giskard.precommit]
PrepareQC_sent_means_PrepareBlock_sent_global [in Giskard.precommit]
PrepareQC_sent_means_PrepareVote_sent_global [in Giskard.precommit]
PrepareQC_sent_means_exists_PrepareVote_processed_local [in Giskard.precommit]
PrepareQC_local_means_vote_quorum_global [in Giskard.prepare]
PrepareVote_sent_means_PrepareBlock_sent_global [in Giskard.precommit]
PrepareVote_sent_means_PrepareBlock_processed_local [in Giskard.precommit]
prepare_stage_in_view_means_PrepareBlock_sent_global [in Giskard.precommit]
prepare_means_PrepareVote_PrepareQC_exists_global [in Giskard.precommit]
prepare_stage_means_prepare_stage_global [in Giskard.precommit]
prepare_stage_in_view_means_prepare_stage_in_view_global [in Giskard.precommit]
prepare_in_view_means_PrepareVote_PrepareQC_exists_global [in Giskard.precommit]
prepare_stage_in_view_persistent_global [in Giskard.precommit]
prepare_stage_in_view_step_global [in Giskard.precommit]
prepare_stage_persistent [in Giskard.precommit]
prepare_in_view_persistent [in Giskard.global]
prepare_stage_process_record_plural_agnostic [in Giskard.local]
prepare_stage_record_plural_agnostic [in Giskard.local]
prepare_stage_record_agnostic [in Giskard.local]
prepare_stage_same_view_height_injective [in Giskard.prepare]
pre_local_evidence_of_equivocation [in Giskard.prepare]
pre_local_evidence_of_equivocation_last_case [in Giskard.prepare]
pre_local_evidence_of_equivocation_middle_case [in Giskard.prepare]
pre_local_means_local_evidence_of_equivocation [in Giskard.prepare]
processed_means_sent_global [in Giskard.global]
processed_means_past_received [in Giskard.global]
processed_ViewChange_in_view_correct [in Giskard.local]
protocol_trace_state_sane [in Giskard.global]
protocol_trace_zero [in Giskard.global]
Q
qc_in_view_persistent [in Giskard.global]qc_current_view_persistent [in Giskard.global]
quorum_growth [in Giskard.structures]
R
remove_subset [in Giskard.lib]S
sent_PrepareVote_means_parent_block_prepare_local [in Giskard.precommit]sent_PrepareVote_means_received_PrepareBlock [in Giskard.global]
sent_PrepareVote_means_received_PrepareBlock [in Giskard.prepare]
state_view_morphism [in Giskard.global]
strongly_wedged_in_between [in Giskard.global]
T
timeout_trigger_message_highest_or_second_highest_global [in Giskard.precommit]timeout_trigger_message_at_least_second_highest_global [in Giskard.precommit]
timeout_trigger_message_global_means_exists_ViewChange_quorum [in Giskard.precommit]
timeout_trigger_message_block_prepare_stage_global [in Giskard.precommit]
trigger_message_view_morphism_global [in Giskard.precommit]
trigger_message_view_morphism_step_global [in Giskard.precommit]
trigger_message_past_exists_global [in Giskard.precommit]
trigger_message_past_step_exists_global [in Giskard.precommit]
trigger_message_block_prepare_stage_global [in Giskard.precommit]
trigger_message_global_backwards_persistent_verbose [in Giskard.precommit]
V
ViewChange_message_block_prepare_stage_global [in Giskard.precommit]ViewChange_quorum_global [in Giskard.global]
view_increment_exists_trigger_message_global [in Giskard.precommit]
view_same_or_plus_one [in Giskard.global]
view_different_tells_receiver [in Giskard.global]
view_state_morphism [in Giskard.global]
view_state_morphism_inductive_step [in Giskard.global]
vote_quorum_in_view_step_global [in Giskard.global]
vote_quorum_local_means_vote_quorum_global [in Giskard.global]
vote_quorum_in_view_global_step [in Giskard.global]
vote_quorum_in_view_persistent [in Giskard.global]
vote_quorum_current_view_persistent [in Giskard.global]
vote_quorum_in_view_step_global [in Giskard.prepare]
vote_quorum_local_means_vote_quorum_global [in Giskard.prepare]
vote_quorum_same_view_global_injective [in Giskard.prepare]
W
wedged_in_between [in Giskard.global]witnessed_quorum_global [in Giskard.prepare]
Constructor Index
D
discard_view_invalid_type [in Giskard.local]G
GState_step_timeout [in Giskard.global]GState_step_process [in Giskard.global]
P
PrepareBlock [in Giskard.structures]PrepareQC [in Giskard.structures]
PrepareVote [in Giskard.structures]
process_PrepareBlock_malicious_vote_type [in Giskard.local]
process_ViewChangeQC_single_type [in Giskard.local]
process_ViewChange_pre_quorum_type [in Giskard.local]
process_ViewChange_quorum_new_proposer_type [in Giskard.local]
process_PrepareQC_non_last_block_type [in Giskard.local]
process_PrepareQC_last_block_type [in Giskard.local]
process_PrepareQC_last_block_new_proposer_type [in Giskard.local]
process_PrepareVote_wait_type [in Giskard.local]
process_PrepareVote_vote_type [in Giskard.local]
process_PrepareBlock_vote_type [in Giskard.local]
process_PrepareBlock_pending_vote_type [in Giskard.local]
process_PrepareBlock_duplicate_type [in Giskard.local]
propose_block_init_type [in Giskard.local]
V
ViewChange [in Giskard.structures]ViewChangeQC [in Giskard.structures]
Axiom Index
A
about_non_last_block [in Giskard.structures]about_generate_last_block [in Giskard.structures]
B
block [in Giskard.structures]block_eqb_correct [in Giskard.structures]
block_eqb [in Giskard.structures]
b_index [in Giskard.structures]
b_height [in Giskard.structures]
E
empty_has_no_one_third' [in Giskard.structures]empty_has_no_two_thirds' [in Giskard.structures]
evil_participants [in Giskard.structures]
G
generate_new_block_parent [in Giskard.structures]generate_last_block [in Giskard.structures]
generate_new_block [in Giskard.structures]
GenesisBlock [in Giskard.structures]
GenesisBlock_height [in Giskard.structures]
H
has_at_least_one_thirdb [in Giskard.structures]has_at_least_two_thirdsb [in Giskard.structures]
honest_nodeb_correct [in Giskard.structures]
honest_nodeb [in Giskard.structures]
honest_node [in Giskard.structures]
I
intersection_property [in Giskard.structures]is_new_proposer_unique [in Giskard.structures]
is_block_proposer [in Giskard.structures]
M
majority_growth [in Giskard.structures]minority_subset [in Giskard.structures]
N
node [in Giskard.structures]node_eqb_correct [in Giskard.structures]
node_eqb [in Giskard.structures]
P
parent_block_height [in Giskard.structures]parent_ofb_correct [in Giskard.structures]
parent_ofb [in Giskard.structures]
parent_of [in Giskard.structures]
participants [in Giskard.structures]
Q
quorum_subset [in Giskard.structures]Inductive Index
G
GState_step [in Giskard.global]M
message_type [in Giskard.structures]N
NState_transition_type [in Giskard.local]Projection Index
C
counting_messages [in Giskard.structures]G
get_piggyback_block [in Giskard.structures]get_block [in Giskard.structures]
get_sender [in Giskard.structures]
get_view [in Giskard.structures]
get_message_type [in Giskard.structures]
I
in_messages [in Giskard.structures]N
node_id [in Giskard.structures]node_view [in Giskard.structures]
O
out_messages [in Giskard.structures]T
timeout [in Giskard.structures]Definition Index
A
add [in Giskard.local]add_plural [in Giskard.local]
at_least_second_highest [in Giskard.precommit]
B
block_eq_dec [in Giskard.structures]broadcast_messages [in Giskard.global]
b_last [in Giskard.structures]
C
commit_height_injective_statement [in Giskard.commit]commit_stage [in Giskard.commit]
D
discard [in Giskard.local]discard_view_invalid [in Giskard.local]
E
equivocating_messages [in Giskard.local]equivocating_in_global_state [in Giskard.prepare]
equivocating_in_state [in Giskard.prepare]
exists_max_prepare_height_in_view_global [in Giskard.precommit]
exists_same_height_blockb [in Giskard.local]
exists_same_height_block_dec [in Giskard.local]
exists_same_height_PrepareBlock [in Giskard.local]
exists_same_height_block [in Giskard.local]
exists_same_height_block_old [in Giskard.local]
F
flip_timeout [in Giskard.local]G
GenesisBlock_message [in Giskard.local]get_transition [in Giskard.local]
GState [in Giskard.global]
GState_sane [in Giskard.global]
GState_transition [in Giskard.global]
GState_init [in Giskard.global]
GTrace [in Giskard.global]
H
has_at_least_one_third [in Giskard.structures]has_at_least_two_thirds [in Giskard.structures]
higher_block [in Giskard.structures]
higher_message [in Giskard.local]
highest_ViewChange_message [in Giskard.local]
highest_message_in_list [in Giskard.local]
highest_prepare_block_message [in Giskard.local]
highest_prepare_block_in_view [in Giskard.local]
highest_ViewChange_block_height_in_view [in Giskard.local]
highest_ViewChange_block_in_view [in Giskard.local]
I
increment_view [in Giskard.local]is_min_prepare_height_in_view [in Giskard.precommit]
is_min_prepare_height_in_view_global [in Giskard.precommit]
is_min_prepare_height_global [in Giskard.precommit]
is_max_prepare_height_in_view [in Giskard.precommit]
is_max_prepare_height_in_view_global [in Giskard.precommit]
is_max_prepare_height_global [in Giskard.precommit]
is_member [in Giskard.structures]
L
last_block [in Giskard.local]M
make_ViewChangeQC [in Giskard.local]make_ViewChange [in Giskard.local]
make_PrepareQC [in Giskard.local]
make_PrepareVote [in Giskard.local]
make_PrepareBlocks [in Giskard.local]
malicious_ignore [in Giskard.local]
message_with_higher_block [in Giskard.structures]
message_eqb [in Giskard.structures]
message_eq_dec [in Giskard.structures]
message_type_eqb [in Giskard.structures]
message_type_eq_dec [in Giskard.structures]
N
node_eq_dec [in Giskard.structures]normal_trigger_message_highest_global_statement [in Giskard.precommit]
normal_trigger_message_global [in Giskard.precommit]
NState_eq_dec [in Giskard.structures]
NState_init [in Giskard.structures]
P
past_view_trigger_message_lowest_block_global_statement [in Giskard.precommit]pending_PrepareVote [in Giskard.local]
precommit_now_height_injective_middle [in Giskard.precommit]
precommit_stage_now_height_injective_statement [in Giskard.precommit]
precommit_stage_now [in Giskard.precommit]
precommit_stage_height_injective_statement [in Giskard.precommit]
precommit_stage [in Giskard.precommit]
PrepareQC_sent_means_exists_PrepareBlock_processed_local [in Giskard.precommit]
PrepareQC_in_view_global [in Giskard.precommit]
PrepareQC_in_view [in Giskard.local]
PrepareVote_about_block_in_view_global [in Giskard.precommit]
PrepareVote_about_block_global [in Giskard.global]
PrepareVote_about_block_in_view_global [in Giskard.global]
prepare_stage_child_non_last [in Giskard.precommit]
prepare_stage_height_view_morphism_global_non_last [in Giskard.precommit]
prepare_stage_height_view_morphism_global [in Giskard.precommit]
prepare_stage_first_parent_highest_or_second_global [in Giskard.precommit]
prepare_stage_global [in Giskard.precommit]
prepare_stage_in_view_global [in Giskard.precommit]
prepare_stage_parent_prepare_stage [in Giskard.precommit]
prepare_stage [in Giskard.local]
prepare_stage_in_viewb [in Giskard.local]
prepare_stage_in_view [in Giskard.local]
prepare_stage_same_view_height_injective_statement [in Giskard.prepare]
pre_local_evidence_of_equivocation_statement [in Giskard.prepare]
pre_equivocating_in_state [in Giskard.prepare]
process [in Giskard.local]
processed_ViewChange_in_view [in Giskard.local]
processed_PrepareVote_in_view_about_block [in Giskard.local]
process_PrepareBlock_malicious_vote [in Giskard.local]
process_ViewChangeQC_single [in Giskard.local]
process_ViewChange_pre_quorum [in Giskard.local]
process_ViewChange_quorum_new_proposer [in Giskard.local]
process_PrepareQC_non_last_block [in Giskard.local]
process_PrepareQC_last_block [in Giskard.local]
process_PrepareQC_last_block_new_proposer [in Giskard.local]
process_PrepareVote_vote [in Giskard.local]
process_PrepareVote_wait [in Giskard.local]
process_PrepareBlock_vote [in Giskard.local]
process_PrepareBlock_pending_vote [in Giskard.local]
process_PrepareBlock_duplicate [in Giskard.local]
process_timeout [in Giskard.local]
propose_block_init [in Giskard.local]
protocol_state [in Giskard.global]
protocol_trace [in Giskard.global]
Q
quorum [in Giskard.structures]quorumb [in Giskard.structures]
R
received [in Giskard.local]record [in Giskard.local]
record_plural [in Giskard.local]
S
same_height_block_msg_dec [in Giskard.local]same_height_block_msg [in Giskard.local]
sent [in Giskard.local]
T
timeout_trigger_message_highest_or_second_highest_global_statement [in Giskard.precommit]timeout_trigger_message_global_dec [in Giskard.precommit]
timeout_trigger_message_global [in Giskard.precommit]
trigger_message_highest_or_second_highest_global_statement [in Giskard.precommit]
trigger_message_next_view_PrepareBlock_same_block_global [in Giskard.precommit]
trigger_message_global [in Giskard.precommit]
V
view_change_quorum_in_view [in Giskard.local]view_validb [in Giskard.local]
view_valid [in Giskard.local]
vote_quorum_in_view_global [in Giskard.precommit]
vote_quorum_in_view_global [in Giskard.global]
vote_quorum_in_view [in Giskard.local]
Record Index
M
message [in Giskard.structures]N
NState [in Giskard.structures]| 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 | (1417 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 | (1077 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 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 | (135 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 | (21 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 | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 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 | (127 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |