proposition: Theorem commitment_hiding : ∀ LA A, ValidPackage LA [interface #val #[ HIDING ] : chHiding → chMessage ] A_export (A ∘ (par KEY (ID Hiding_E))) → fdisjoint LA KEY_locs -> fdisjoint LA Sigma_to_Com_locs -> fdisjoint LA (fset [:: setup_loc]) -> fdisjoint LA Sigma_locs -> fdisjoint LA Simulator_locs -> fdisjoint Simulator_locs (fset [:: statement_loc ; witness_loc]) -> fdisjoint Sigma_locs (fset [:: statement_loc ; witness_loc]) -> (ɛ_hiding A) <= 0 + AdvantageE SHVZK_ideal SHVZK_real (((A ∘ par KEY (ID Hiding_E)) ∘ Hiding_real) ∘ Sigma_to_Com_Aux) + AdvantageE (Hiding_real ∘ Sigma_to_Com_Aux ∘ SHVZK_real) (Hiding_ideal ∘ Sigma_to_Com_Aux ∘ SHVZK_real) (A ∘ par KEY (ID Hiding_E)) + AdvantageE SHVZK_real SHVZK_ideal (((A ∘ par KEY (ID Hiding_E)) ∘ Hiding_ideal) ∘ Sigma_to_Com_Aux) + 0.
proof: Proof. unfold ɛ_hiding, ɛ_SHVZK. intros LA A VA Hd1 Hd2 Hd3 HdSigma HdSimulator Hd4 Hd5. ssprove triangle (Hiding_real ∘ Sigma_to_Com ∘ KEY) [:: (Hiding_real ∘ Sigma_to_Com_Aux ∘ SHVZK_ideal) ; (Hiding_real ∘ Sigma_to_Com_Aux ∘ SHVZK_real) ; (Hiding_ideal ∘ Sigma_to_Com_Aux ∘ SHVZK_real) ; (Hiding_ideal ∘ Sigma_to_Com_Aux ∘ SHVZK_ideal) ] (Hiding_ideal ∘ Sigma_to_Com ∘ KEY) (A ∘ (par KEY (ID Hiding_E))) as ineq. eapply le_trans. 1: exact ineq. clear ineq. repeat eapply ler_add. - apply eq_ler. eapply eq_rel_perf_ind with (inv := inv). 5: apply VA. 1:{ ssprove_valid. 3: apply fsub0set. 3: apply fsubsetxx. 1: instantiate (1 := (Sigma_to_Com_locs :|: KEY_locs)). 1: apply fsubsetUl. 1: apply fsubsetUr. } 1:{ ssprove_valid. 1: apply fsubsetxx. 2: apply fsub0set. 2: apply fsubsetxx. unfold Sigma_to_Com_locs. apply fsubsetU ; apply /orP ; right. apply fsubsetUr. } 3,4: rewrite fdisjointUr ; apply /andP ; split. 3-4,6: assumption. 3: rewrite fset1E ; assumption. 1: exact _. rewrite Sigma_to_Com_equation_1. rewrite Sigma_to_Com_Aux_equation_1. simplify_eq_rel h. ssprove_code_simpl. destruct h. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=>b. case (Nat.even b) eqn:Hb ; rewrite Hb. + ssprove_sync=> setup. ssprove_code_simpl. ssprove_code_simpl_more. apply r_assertD. 1: done. intros _ _. ssprove_sync=> w. apply r_assertD. 1: done. intros _ Rel. ssprove_swap_seq_lhs [:: 2 ; 1]%N. ssprove_contract_put_get_lhs. rewrite !cast_fun_K. rewrite Rel. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync. ssprove_swap_lhs 1%N. ssprove_contract_put_get_lhs. ssprove_swap_seq_lhs [:: 0 ; 1]%N. ssprove_contract_put_get_lhs. apply r_put_lhs. apply r_put_lhs. ssprove_restore_pre. 1: ssprove_invariant. eapply rsame_head_alt. 1: exact _. { unfold inv. intros l lin h1 s' h2. apply h2. move: Hd4 => /fdisjointP Hd4. apply Hd4. apply lin. } { unfold inv. intros l v lin. apply put_pre_cond_heap_ignore. } intros t. destruct t. destruct s1. destruct s1. ssprove_sync. ssprove_sync. apply r_ret. done. + ssprove_sync=>setup. ssprove_code_simpl. ssprove_code_simpl_more. apply r_assertD. 1: done. intros _ _. ssprove_sync=>w. apply r_assertD. 1: done. intros _ Rel. ssprove_swap_seq_lhs [:: 2 ; 1]%N. ssprove_contract_put_get_lhs. rewrite !cast_fun_K. rewrite Rel. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync. ssprove_swap_lhs 1%N. ssprove_contract_put_get_lhs. ssprove_swap_seq_lhs [:: 0 ; 1]%N. ssprove_contract_put_get_lhs. apply r_put_lhs. apply r_put_lhs. ssprove_restore_pre. 1: ssprove_invariant. eapply rsame_head_alt. 1: exact _. { unfold inv. intros l lin h1 s' h2. apply h2. move: Hd4 => /fdisjointP Hd4. apply Hd4. apply lin. } { unfold inv. intros l v lin. apply put_pre_cond_heap_ignore. } intros t. destruct t. destruct s1. destruct s1. ssprove_sync. ssprove_sync. apply r_ret. done. - rewrite -!Advantage_link. 1: apply eq_ler ; done. - done. - rewrite -!Advantage_link. 1: apply eq_ler ; done. - apply eq_ler. eapply eq_rel_perf_ind with (inv := inv). 5: apply VA. 1:{ ssprove_valid. 4: apply fsubsetxx. 3: apply fsub0set. 2: instantiate (1 := (Simulator_locs :|: (setup_loc |: Sigma_to_Com_locs))). - apply fsubsetUr. - apply fsubsetUl. } 1:{ ssprove_valid. 3: apply fsub0set. 3: apply fsubsetxx. 1: instantiate (1 := (Sigma_to_Com_locs :|: KEY_locs)). - apply fsubsetUl. - apply fsubsetUr. } 3,4: rewrite fdisjointUr ; apply /andP ; split. 4: rewrite fdisjointUr ; apply /andP ; split. 3,5-7: assumption. 3: rewrite fset1E ; assumption. { ssprove_invariant. unfold KEY_locs. apply fsubsetU ; apply /orP ; right. apply fsubsetU ; apply /orP ; right. rewrite !fset_cons. apply fsubsetU ; apply /orP ; right. rewrite fsubUset ; apply /andP ; split. - apply fsubsetU ; apply /orP ; right. apply fsubsetU ; apply /orP ; left. apply fsubsetxx. - apply fsubsetU ; apply /orP ; left. rewrite fsubUset ; apply /andP ; split. + apply fsubsetxx. + rewrite -fset0E. apply fsub0set. } rewrite Sigma_to_Com_equation_1. rewrite Sigma_to_Com_Aux_equation_1. simplify_eq_rel h. ssprove_code_simpl. destruct h. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync=>e. ssprove_sync=> setup. ssprove_code_simpl. ssprove_code_simpl_more. apply r_assertD. 1: done. intros _ _. ssprove_sync=> w. apply r_assertD. 1: done. intros _ Rel. ssprove_swap_seq_rhs [:: 2 ; 1]%N. ssprove_contract_put_get_rhs. rewrite !cast_fun_K. rewrite Rel. ssprove_code_simpl. ssprove_code_simpl_more. ssprove_sync. ssprove_swap_rhs 1%N. ssprove_contract_put_get_rhs. ssprove_swap_seq_rhs [:: 0 ; 1]%N. ssprove_contract_put_get_rhs. apply r_put_rhs. apply r_put_rhs. ssprove_restore_pre. 1: ssprove_invariant. eapply rsame_head_alt. 1: exact _. { unfold inv. intros l lin h1 s' h2. apply h2. move: Hd4 => /fdisjointP Hd4. apply Hd4. apply lin. } { unfold inv. intros l v lin. apply put_pre_cond_heap_ignore. } intros t. destruct t. destruct s1. destruct s1. ssprove_sync. ssprove_sync. apply r_ret. done. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)