Lemma Dependencies

Badge Legend: M Main Result T Theorem H Helper Lemma
322
Lemmas
0
Dependencies
0
With Dependencies
22
Files
10,609
Lines
bec7c86
Source Commit
Lemma File Section #Uses #By Uses (from stats)
H dsdp_ok dumas2017dual/dsdp/dsdp_correctness.v dsdp_computational 0 0 No dependencies in stats
H dsdp_traces_ok dumas2017dual/dsdp/dsdp_correctness.v dsdp_computational 0 0 No dependencies in stats
H dsdp_is_correct dumas2017dual/dsdp/dsdp_correctness.v dsdp_computational 0 0 No dependencies in stats
T dsdp_computes_dot_product_benaloh dumas2017dual/dsdp/dsdp_correctness.v dsdp_computational_benaloh 0 0 No dependencies in stats
T dsdp_computes_dot_product_paillier dumas2017dual/dsdp/dsdp_correctness.v dsdp_computational_paillier 0 0 No dependencies in stats
H dsdp_fiber_card dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy 0 0 No dependencies in stats
H Pr_dsdp_nosol_eq0 dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy 0 0 No dependencies in stats
H Pr_dsdp_sol_uniform dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy 0 0 No dependencies in stats
H dsdp_centropy1_uniform dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy 0 0 No dependencies in stats
T dsdp_centropy_uniform dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy 0 0 No dependencies in stats
H dsdp_var_entropy dumas2017dual/dsdp/dsdp_entropy.v dsdp_var_entropy 0 0 No dependencies in stats
H dsdp_fiber_card_n dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy_n 0 0 No dependencies in stats
H dsdp_centropy1_uniform_n dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy_n 0 0 No dependencies in stats
T dsdp_centropy_uniform_n dumas2017dual/dsdp/dsdp_entropy.v dsdp_entropy_n 0 0 No dependencies in stats
H U3_nonzero dumas2017dual/dsdp/dsdp_entropy.v functional_determination 0 0 No dependencies in stats
M V3_determined dumas2017dual/dsdp/dsdp_entropy.v functional_determination 0 0 No dependencies in stats
H V3_determined_centropy_v2 dumas2017dual/dsdp/dsdp_entropy.v functional_determination 0 0 No dependencies in stats
H alice_view_to_cond dumas2017dual/dsdp/dsdp_entropy.v semi_honest_case_analysis 0 0 No dependencies in stats
H joint_centropy_reduction dumas2017dual/dsdp/dsdp_entropy.v semi_honest_case_analysis 0 0 No dependencies in stats
T dsdp_result_correct dumas2017dual/dsdp/dsdp_entropy_trace.v dsdp_traces 0 0 No dependencies in stats
H dsdp_algebraic_correctness dumas2017dual/dsdp/dsdp_entropy_trace.v trace_entropy_analysis 0 0 No dependencies in stats
H dsdp_dtype_eqP dumas2017dual/dsdp/dsdp_interface.v Top-level 0 0 No dependencies in stats
H std_from_enc_e dumas2017dual/dsdp/dsdp_interface.v Standard_Interface_Properties 0 0 No dependencies in stats
H std_from_enc_d dumas2017dual/dsdp/dsdp_interface.v Standard_Interface_Properties 0 0 No dependencies in stats
H std_from_enc_k dumas2017dual/dsdp/dsdp_interface.v Standard_Interface_Properties 0 0 No dependencies in stats
H alice_cross_eq dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H bob_cross_eq dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H charlie_cross_eq dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H alice_bob_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H alice_charlie_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H bob_charlie_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H pbob_is_first dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H pcharlie_is_last dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H alice_bob_tmpl_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H alice_charlie_tmpl_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H bob_charlie_tmpl_dual dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H dsdp_max_fuel_ok dumas2017dual/dsdp/dsdp_pismc.v smc_dsdp_program 0 0 No dependencies in stats
H dsdp_ideal_max_fuel_ok dumas2017dual/dsdp/dsdp_pismc.v dsdp_idealized_termination 0 0 No dependencies in stats
H dsdp_ideal_terminates dumas2017dual/dsdp/dsdp_pismc.v dsdp_idealized_termination 0 0 No dependencies in stats
H dsdp_ideal_no_fail dumas2017dual/dsdp/dsdp_pismc.v dsdp_idealized_termination 0 0 No dependencies in stats
T dsdp_ideal_senv_zero dumas2017dual/dsdp/dsdp_pismc.v dsdp_idealized_termination 0 0 No dependencies in stats
H alice_first_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H alice_inter_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H alice_last_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H first_inter_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H first_last_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H inter_last_dual_n4 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H dsdp_n4_builder_correct dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H dsdp_n4_max_fuel_ok dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H dsdp_n4_terminates dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H dsdp_n4_no_fail dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
T dsdp_n4_senv_zero dumas2017dual/dsdp/dsdp_pismc.v dsdp_n4_idealized_duality 0 0 No dependencies in stats
H alice_first_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H alice_inter2_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H alice_inter3_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H alice_last_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H first_inter2_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H first_inter3_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H first_last_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H inter2_inter3_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H inter2_last_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H inter3_last_dual_n5 dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H dsdp_n5_terminates dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H dsdp_n5_no_fail dumas2017dual/dsdp/dsdp_pismc.v dsdp_n5_idealized_duality 0 0 No dependencies in stats
H size_dsdp_n_procs dumas2017dual/dsdp/dsdp_pismc.v dsdp_n_rsteps 0 0 No dependencies in stats
H palice_n_erase dumas2017dual/dsdp/dsdp_pismc.v dsdp_n_rsteps 0 0 No dependencies in stats
H DParty_first_erase dumas2017dual/dsdp/dsdp_pismc.v dsdp_n_rsteps 0 0 No dependencies in stats
H DParty_last_erase dumas2017dual/dsdp/dsdp_pismc.v dsdp_n_rsteps 0 0 No dependencies in stats
H DParty_intermediate_erase dumas2017dual/dsdp/dsdp_pismc.v dsdp_n_rsteps 0 0 No dependencies in stats
H size_interp1 dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H step_proc_trace_indep dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H step_progress_trace_indep dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H interp1E dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H step_iota_enum dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H interp_sound dumas2017dual/dsdp/dsdp_pismc.v interp_sound_section 0 0 No dependencies in stats
H dsdp_3party_terminates dumas2017dual/dsdp/dsdp_pismc.v dsdp_3party_rsteps 0 0 No dependencies in stats
H dsdp_3party_no_fail dumas2017dual/dsdp/dsdp_pismc.v dsdp_3party_rsteps 0 0 No dependencies in stats
T dsdp_3party_rsteps dumas2017dual/dsdp/dsdp_pismc.v dsdp_3party_rsteps 0 0 No dependencies in stats
H alice_a2_value dumas2017dual/dsdp/dsdp_program.v dsdp 0 0 No dependencies in stats
H alice_a3_value dumas2017dual/dsdp/dsdp_program.v dsdp 0 0 No dependencies in stats
H bob_combined_value dumas2017dual/dsdp/dsdp_program.v dsdp 0 0 No dependencies in stats
T dsdp_computes_dot_product dumas2017dual/dsdp/dsdp_program.v dsdp 0 0 No dependencies in stats
T dsdp_computes_dot_product_n dumas2017dual/dsdp/dsdp_program.v dsdp_n 0 0 No dependencies in stats
T dsdp_constraint_centropy_eqlogm dumas2017dual/dsdp/dsdp_security.v dsdp_security 0 0 No dependencies in stats
H V3_determined_centropy_v2_local dumas2017dual/dsdp/dsdp_security.v dsdp_security 0 0 No dependencies in stats
T dsdp_entropic_security dumas2017dual/dsdp/dsdp_security.v dsdp_security 0 0 No dependencies in stats
H S_E dumas2017dual/dsdp/dsdp_security.v dotp2 0 0 No dependencies in stats
M ConstUS_discloses_V2 dumas2017dual/dsdp/dsdp_security.v malicious_adversary_case_analysis 0 0 No dependencies in stats
T US_compromised_leaks_V2 dumas2017dual/dsdp/dsdp_security.v malicious_adversary_case_analysis 0 0 No dependencies in stats
H U3_R3_indep_V1 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H VU3_indep_V1 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H VU3R_indep_V1 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H E_charlie_vur3_indep_V1 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H E_bob_d2_indep_V1 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
T BobView_indep_V1_proven dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H D2_indep_V3 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
H E_bob_d2_indep_V3 dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
T BobView_indep_V3_proven dumas2017dual/dsdp/dsdp_security.v bob_security_independence 0 0 No dependencies in stats
T bob_privacy_V1_alt dumas2017dual/dsdp/dsdp_security.v bob_security 0 0 No dependencies in stats
T bob_privacy_V1 dumas2017dual/dsdp/dsdp_security.v bob_security 0 0 No dependencies in stats
T bob_privacy_V3_alt dumas2017dual/dsdp/dsdp_security.v bob_security 0 0 No dependencies in stats
T bob_privacy_V3 dumas2017dual/dsdp/dsdp_security.v bob_security 0 0 No dependencies in stats
H D2_indep_V2 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H D2_indep_VU3R_V2 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H D3_indep_V2 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H E_charlie_d3_indep_V2 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
T CharlieView_indep_V2_proven dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H V2V3_indep_V1 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H V1_indep_U2U3R2R3 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H alice_indep_no_Dka dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H alice_indep_no_Dka_U1 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H V2V3_indep_V1_randoms dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H V2V3_indep_V1_randoms_structured dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
M D3_indep_V1 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
H E_charlie_d3_indep_V1 dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
T CharlieView_indep_V1_proven dumas2017dual/dsdp/dsdp_security.v charlie_security_independence 0 0 No dependencies in stats
T charlie_privacy_V1_alt dumas2017dual/dsdp/dsdp_security.v charlie_security 0 0 No dependencies in stats
T charlie_privacy_V1 dumas2017dual/dsdp/dsdp_security.v charlie_security 0 0 No dependencies in stats
T charlie_privacy_V2_alt dumas2017dual/dsdp/dsdp_security.v charlie_security 0 0 No dependencies in stats
T charlie_privacy_V2 dumas2017dual/dsdp/dsdp_security.v charlie_security 0 0 No dependencies in stats
H relay_otp_indep dumas2017dual/dsdp/dsdp_security.v relay_security_n 0 0 No dependencies in stats
H relay_enc_otp_indep dumas2017dual/dsdp/dsdp_security.v relay_security_n 0 0 No dependencies in stats
H relay_privacy_from_indep dumas2017dual/dsdp/dsdp_security.v relay_security_n 0 0 No dependencies in stats
H relay_privacy_logm dumas2017dual/dsdp/dsdp_security.v relay_security_n 0 0 No dependencies in stats
T enc_ce_contract_ind dumas2017dual/dsdp/dsdp_security.v enc_contraction_n 0 0 No dependencies in stats
T dsdp_entropic_security_n_eq dumas2017dual/dsdp/dsdp_security.v dsdp_security_n 0 0 No dependencies in stats
T dsdp_entropic_security_n dumas2017dual/dsdp/dsdp_security.v dsdp_security_n 0 0 No dependencies in stats
H dotp_n_e1 dumas2017dual/dsdp/dsdp_security.v malicious_n 0 0 No dependencies in stats
H ConstUS_n_discloses_V1 dumas2017dual/dsdp/dsdp_security.v malicious_n 0 0 No dependencies in stats
H test_init_space_eq dumas2017dual/dsdp/dsdp_syntax_demo.v tests 0 0 No dependencies in stats
H test_init_tuple_eq dumas2017dual/dsdp/dsdp_syntax_demo.v tests 0 0 No dependencies in stats
H test_init_chained_eq dumas2017dual/dsdp/dsdp_syntax_demo.v tests 0 0 No dependencies in stats
H test_recv_lambda_eq dumas2017dual/dsdp/dsdp_syntax_demo.v tests 0 0 No dependencies in stats
H test_recv_dec_eq dumas2017dual/dsdp/dsdp_syntax_demo.v recv_dec_enc_tests 0 0 No dependencies in stats
H test_recv_enc_eq dumas2017dual/dsdp/dsdp_syntax_demo.v recv_dec_enc_tests 0 0 No dependencies in stats
H test_key_wrapper_eq dumas2017dual/dsdp/dsdp_syntax_demo.v wrapper_tests 0 0 No dependencies in stats
H test_data_wrapper_eq dumas2017dual/dsdp/dsdp_syntax_demo.v wrapper_tests 0 0 No dependencies in stats
H test_enc_wrapper_eq dumas2017dual/dsdp/dsdp_syntax_demo.v wrapper_tests 0 0 No dependencies in stats
H partyA_structure dumas2017dual/dsdp/dsdp_syntax_demo.v two_party_example 0 0 No dependencies in stats
H partyB_structure dumas2017dual/dsdp/dsdp_syntax_demo.v two_party_example 0 0 No dependencies in stats
H unicode_ascii_eq dumas2017dual/dsdp/dsdp_syntax_demo.v unicode_vs_ascii 0 0 No dependencies in stats
H mixed_eq dumas2017dual/dsdp/dsdp_syntax_demo.v unicode_vs_ascii 0 0 No dependencies in stats
H mem_image_set dumas2017dual/entropy_fiber/entropy_fiber.v abstract_fibers 0 0 No dependencies in stats
H fiber_non_empty_image dumas2017dual/entropy_fiber/entropy_fiber.v abstract_fibers 0 0 No dependencies in stats
H mem_fiber dumas2017dual/entropy_fiber/entropy_fiber.v abstract_fibers 0 0 No dependencies in stats
H nmem_fiber dumas2017dual/entropy_fiber/entropy_fiber.v abstract_fibers 0 0 No dependencies in stats
M centropy1_uniform_over_set dumas2017dual/entropy_fiber/entropy_fiber.v general_pointwise_entropy 0 0 No dependencies in stats
H fiberC_cond_Pr0 dumas2017dual/entropy_fiber/entropy_fiber.v fiber_entropy 0 0 No dependencies in stats
M centropy1_as_sum dumas2017dual/entropy_fiber/entropy_fiber.v fiber_entropy 0 0 No dependencies in stats
H entropy_uniform_set dumas2017dual/entropy_fiber/entropy_fiber.v fiber_entropy 0 0 No dependencies in stats
H entropy_fdist_uniform_set dumas2017dual/entropy_fiber/entropy_fiber.v fiber_entropy 0 0 No dependencies in stats
M centropy1_uniform_fiber dumas2017dual/entropy_fiber/entropy_fiber.v fiber_entropy 0 0 No dependencies in stats
H centropy_constant_fibers dumas2017dual/entropy_fiber/entropy_fiber.v constant_fiber_size 0 0 No dependencies in stats
M centropy_determined_contract dumas2017dual/entropy_fiber/entropy_fiber.v functional_determinacy 0 0 No dependencies in stats
H fiberC_jcond_Pr0 dumas2017dual/entropy_fiber/entropy_fiber.v conditional_entropy_with_functional_constraint 0 0 No dependencies in stats
H centropy_jcond_determined_fibers dumas2017dual/entropy_fiber/entropy_fiber.v conditional_entropy_with_functional_constraint 0 0 No dependencies in stats
H joint_factors_by_indeE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v fiber_entropy 0 0 No dependencies in stats
H uniform_VarRV_probE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v fiber_entropy 0 0 No dependencies in stats
H Pr_cond_fiber_marginE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v marginal_probability 0 0 No dependencies in stats
M cPr_uniform_fiber dumas2017dual/entropy_fiber/entropy_fiber_zpq.v conditional_probability 0 0 No dependencies in stats
H gen_joint_factors_by_indeE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v fiber_entropy_gen 0 0 No dependencies in stats
H gen_uniform_VarRV_probE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v fiber_entropy_gen 0 0 No dependencies in stats
H gen_Pr_cond_fiber_marginE dumas2017dual/entropy_fiber/entropy_fiber_zpq.v gen_marginal_probability 0 0 No dependencies in stats
H gen_cPr_uniform_fiber dumas2017dual/entropy_fiber/entropy_fiber_zpq.v gen_conditional_probability 0 0 No dependencies in stats
H proj_Fp_add dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fp_mul dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fq_add dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fq_mul dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H fiber_Fp_card dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H fiber_Fq_card dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H val_Fp_lt_p dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H val_Fq_lt_q dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H val_msg_lt_m dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H chinese_proj_p dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H chinese_proj_q dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fp_crt dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fq_crt dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_proj_id dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H chinese_mod_inj_p dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H chinese_mod_inj_q dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_pair_inj dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H constraint_proj dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H constraint_crt dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fp_neq0 dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H proj_Fq_neq0 dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_proj_pair_inj dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_proj_pair_fiber dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_pair_fiber dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H crt_proj_pair_surj dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
M linear_fiber_2d_card dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_2d 0 0 No dependencies in stats
H lt_minpq_coprime dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H coprime_unitZm dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H widen_lift_ord_max dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H sum_split_last dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H extend_in_fiber dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H project_extend_id dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H extend_project_id dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H extend_fiber_inj dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
M linear_fiber_nd_card dumas2017dual/entropy_fiber/linear_fiber_zpq.v fiber_nd 0 0 No dependencies in stats
H logr_eq1 dumas2017dual/lib/extra_algebra.v log_extra 0 0 No dependencies in stats
H bigD1_filter dumas2017dual/lib/extra_algebra.v bigop_extra 0 0 No dependencies in stats
H bigD1_seq_cond dumas2017dual/lib/extra_algebra.v bigop_extra 0 0 No dependencies in stats
M coprime_Zp_unit dumas2017dual/lib/extra_algebra.v Zp_unit_extra 0 0 No dependencies in stats
H Zp_unit_coprime dumas2017dual/lib/extra_algebra.v Zp_unit_extra 0 0 No dependencies in stats
H Zp_unitP dumas2017dual/lib/extra_algebra.v Zp_unit_extra 0 0 No dependencies in stats
H Zp_Fp_card_eq dumas2017dual/lib/extra_algebra.v Zp_Fp_equivalence 0 0 No dependencies in stats
H entropy_formula_same dumas2017dual/lib/extra_algebra.v Zp_Fp_equivalence 0 0 No dependencies in stats
H entropy_sum_split dumas2017dual/lib/extra_entropy.v entropy_sum 0 0 No dependencies in stats
H cinde_cond_mutual_info0 dumas2017dual/lib/extra_entropy.v cinde_cond_mutual_info0 0 0 No dependencies in stats
M cinde_centropy_eq dumas2017dual/lib/extra_entropy.v cinde_centropy_eq 0 0 No dependencies in stats
H zero_entropy_eq_point_mass1 dumas2017dual/lib/extra_entropy.v zero_entropy_eq_point_mass 0 0 No dependencies in stats
H zero_entropy_eq_point_mass dumas2017dual/lib/extra_entropy.v zero_entropy_eq_point_mass 0 0 No dependencies in stats
H centropy_term_deterministic dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
H jfdist_cond_entropy_zero dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
H point_mass_to_cond_prob dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
H zero_centropy1_point_mass dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
M zero_centropy_eq_deterministic1 dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
M zero_centropy_eq_deterministic dumas2017dual/lib/extra_entropy.v zero_centropy_eq_point_mass 0 0 No dependencies in stats
H inde_cond_entropy dumas2017dual/lib/extra_entropy.v inde_entropy_lemmas 0 0 No dependencies in stats
H pair_notin_fin_img_fst dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H sum_cPr_eq dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H cPr_eq_notin_fin_img dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H cPr_eq_two_ones_absurd dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H jfdist_cond_cPr_eq dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H cond_prob_zero_outside_constraint dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H PrX_fstRV dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H jproduct_ruleRV dumas2017dual/lib/extra_proba.v proba_extra 0 0 No dependencies in stats
H fdist_proj23_RV3 dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H pfwd1_pair4_swap34 dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H pfwd1_nested3_AC dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H pfwd1_pair4_mid_A dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H centropyAC dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H centropyA dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H centropyA_middle dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H centropy4_swap_2_4 dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
H marginal_swap_YZ dumas2017dual/lib/extra_proba.v perm_extra 0 0 No dependencies in stats
M card_vspace dumas2017dual/lib/rouche_capelli.v finvect_lemmas 0 0 No dependencies in stats
H card_lker_lfun dumas2017dual/lib/rouche_capelli.v finvect_lemmas 0 0 No dependencies in stats
H diffvv dumas2017dual/lib/rouche_capelli.v vector_ext 0 0 No dependencies in stats
H limg_lker dumas2017dual/lib/rouche_capelli.v vector_ext 0 0 No dependencies in stats
H HomK dumas2017dual/lib/rouche_capelli.v vector_ext 0 0 No dependencies in stats
M mxrank_sub_eqmx dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H rouche1 dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H rouche2 dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H exists_nonzero_kernel dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H kernel_membership dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H kernel_coeff_exists dumas2017dual/lib/rouche_capelli.v RoucheCapelliTheorems 0 0 No dependencies in stats
H sub_coker_colspan dumas2017dual/lib/rouche_capelli.v FiniteSolutionCounting 0 0 No dependencies in stats
H submx_castmx dumas2017dual/lib/rouche_capelli.v FiniteSolutionCounting 0 0 No dependencies in stats
H castmx_mul_row dumas2017dual/lib/rouche_capelli.v FiniteSolutionCounting 0 0 No dependencies in stats
H card_lker_mxof dumas2017dual/lib/rouche_capelli.v card_lker 0 0 No dependencies in stats
H dim_rV dumas2017dual/lib/rouche_capelli.v counting 0 0 No dependencies in stats
H card_lker_Hom dumas2017dual/lib/rouche_capelli.v counting 0 0 No dependencies in stats
H cancel_row_free dumas2017dual/lib/rouche_capelli.v counting 0 0 No dependencies in stats
H row_free_tr dumas2017dual/lib/rouche_capelli.v counting 0 0 No dependencies in stats
H count_kernel_vectors dumas2017dual/lib/rouche_capelli.v counting 0 0 No dependencies in stats
H affine_eq_translate_kernel dumas2017dual/lib/rouche_capelli.v affine_solution_counting 0 0 No dependencies in stats
H card_translate dumas2017dual/lib/rouche_capelli.v affine_solution_counting 0 0 No dependencies in stats
H count_affine_solutions dumas2017dual/lib/rouche_capelli.v affine_solution_counting 0 0 No dependencies in stats
M count_affine_solutions_explicit dumas2017dual/lib/rouche_capelli.v affine_solution_counting 0 0 No dependencies in stats
H affine_eq_translate_kernel_col dumas2017dual/lib/rouche_capelli.v affine_solultion_counting_col 0 0 No dependencies in stats
H card_translate_col dumas2017dual/lib/rouche_capelli.v affine_solultion_counting_col 0 0 No dependencies in stats
H count_affine_solutions_col dumas2017dual/lib/rouche_capelli.v affine_solultion_counting_col 0 0 No dependencies in stats
H count_kernel_vectors_col dumas2017dual/lib/rouche_capelli.v affine_solultion_counting_col 0 0 No dependencies in stats
M count_affine_solutions_explicit_col dumas2017dual/lib/rouche_capelli.v affine_solultion_counting_col 0 0 No dependencies in stats
H count_affine_solutions_rank1 dumas2017dual/lib/rouche_capelli.v FiniteSolutionCounting 0 0 No dependencies in stats
H dec_correct_mixin homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H Emul_addM homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H Epow_scalarM homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H benaloh_Emul_assoc homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H benaloh_Emul_comm homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H benaloh_Emul_id homomorphic_encryption/benaloh1994/benaloh_ahe.v benaloh_instance 0 0 No dependencies in stats
H Zp_add_eqmod homomorphic_encryption/benaloh1994/benaloh_enc.v Top-level 0 0 No dependencies in stats
H Zp_mulrn_nat homomorphic_encryption/benaloh1994/benaloh_enc.v Top-level 0 0 No dependencies in stats
H Zp_mulrn_eqmod homomorphic_encryption/benaloh1994/benaloh_enc.v Top-level 0 0 No dependencies in stats
H val_unit_exp homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H euler_unit homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H expr_modr homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H Zp_val_ltn homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H enc_mul_dist homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H enc_exp_dist homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H alpha_phi homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H rth_powers_vanish homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H ciphertext_to_alpha homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H decryption_unique homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H benaloh_dec_correct homomorphic_encryption/benaloh1994/benaloh_enc.v BenalohEuler 0 0 No dependencies in stats
H party_id_eqP homomorphic_encryption/homomorphic_encryption.v party_id_def 0 0 No dependencies in stats
H party_id_natK homomorphic_encryption/homomorphic_encryption.v party_id_def 0 0 No dependencies in stats
H party_id_enumP homomorphic_encryption/homomorphic_encryption.v party_id_def 0 0 No dependencies in stats
H card_party_key homomorphic_encryption/homomorphic_encryption.v party_key_types 0 0 No dependencies in stats
H card_enc_for homomorphic_encryption/homomorphic_encryption.v enc_types 0 0 No dependencies in stats
H card_enc_for homomorphic_encryption/homomorphic_encryption.v enc_types 0 0 No dependencies in stats
H E_enc_ce_contract homomorphic_encryption/homomorphic_encryption.v enc_lemmas 0 0 No dependencies in stats
H idealized_dec_correct homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H idealized_Emul_addM homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H idealized_Epow_scalarM homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H idealized_Emul_assoc homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H idealized_Emul_comm homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H idealized_Emul_id homomorphic_encryption/idealized/idealized_ahe.v Idealized_AHE 0 0 No dependencies in stats
H key_type_eqP homomorphic_encryption/key_type.v key_type_def 0 0 No dependencies in stats
H key_type_natK homomorphic_encryption/key_type.v key_type_def 0 0 No dependencies in stats
H key_type_enumP homomorphic_encryption/key_type.v key_type_def 0 0 No dependencies in stats
H paillier_dec_correct_mixin homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H paillier_Emul_addM homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H paillier_Epow_scalarM homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H paillier_Emul_assoc homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H paillier_Emul_comm homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H paillier_Emul_id homomorphic_encryption/paillier1999/paillier_ahe.v paillier_instance 0 0 No dependencies in stats
H Zp_add_eqmod homomorphic_encryption/paillier1999/paillier_enc.v Top-level 0 0 No dependencies in stats
H Zp_mulrn_nat homomorphic_encryption/paillier1999/paillier_enc.v Top-level 0 0 No dependencies in stats
H Zp_mulrn_eqmod homomorphic_encryption/paillier1999/paillier_enc.v Top-level 0 0 No dependencies in stats
H val_unit_exp homomorphic_encryption/paillier1999/paillier_enc.v Top-level 0 0 No dependencies in stats
H val_unit_mul homomorphic_encryption/paillier1999/paillier_enc.v Top-level 0 0 No dependencies in stats
H n2_gt1 homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H expr_modn homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H enc_mul_dist homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H enc_exp_dist homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H euler_unit homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H nth_powers_vanish homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H ciphertext_to_lambda homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
H decryption_unique homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats
M paillier_dec_correct homomorphic_encryption/paillier1999/paillier_enc.v paillier_params 0 0 No dependencies in stats