proposition: Lemma extractor_success: ∀ LA A, ValidPackage LA [interface #val #[ SOUNDNESS ] : chSoundness → 'bool ] A_export A → ɛ_soundness A = 0.
proof: Proof. intros LA A VA. apply: eq_rel_perf_ind_eq. 2,3: apply fdisjoints0. simplify_eq_rel h. destruct h as [? [? [? [? [? ?]]]]]. destruct s1. case [&& _ & _] eqn:e. all: apply r_ret; auto. intros h1 h2 ->. unfold R. unfold "&&" in e. inversion e. repeat match goal with | |- context [ if ?b then _ else _ ] => case b eqn:? end. 2,3: discriminate. rewrite otf_fto in Heqs4. rewrite otf_fto in e. apply reflection_nonsense in e. apply reflection_nonsense in Heqs4. rewrite H0. rewrite otf_fto expg_mod. 2: rewrite order_ge1 ; apply expg_order. rewrite expgM expg_mod. 2: rewrite order_ge1 ; apply expg_order. rewrite expgD -FinRing.zmodVgE expg_zneg. 2: apply cycle_id. rewrite Heqs4 e !expgMn. 2-3: apply group_prodC. rewrite invMg !expgMn. 2: apply group_prodC. rewrite !group_prodA. rewrite group_prodC 2!group_prodA -expgMn. 2: apply group_prodC. rewrite mulVg expg1n mul1g -expg_zneg. 2:{ have Hx : exists ix, otf s = g ^+ ix. { apply /cycleP. rewrite -g_gen. apply: in_setT. } destruct Hx as [ix ->]. apply mem_cycle. } rewrite expgAC. rewrite [otf s ^+ (- otf s2) ^+ _] expgAC. rewrite -expgD -expgM. have <- := @expg_mod _ q. 2:{ have Hx : exists ix, otf s = g ^+ ix. { apply /cycleP. rewrite -g_gen. apply: in_setT. } destruct Hx as [ix ->]. rewrite expgAC /q. rewrite expg_order. apply expg1n. } rewrite -modnMmr. have -> : (modn (addn (@nat_of_ord (S (S (Zp_trunc q))) (@otf Challenge s1)) (@nat_of_ord (S (S (Zp_trunc q))) (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q)))) (@otf Challenge s2)))) q) = (@nat_of_ord (S (S (Zp_trunc q))) (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))). { simpl. rewrite modnDmr. destruct (otf s2) as [a Ha]. destruct a as [| Pa]. - simpl. rewrite subn0 modnn addn0 modnDr. rewrite -> order_ge1 at 3. rewrite modn_small. + reflexivity. + rewrite <- order_ge1 at 2. apply ltn_ord. - simpl. rewrite <- order_ge1 at 4. rewrite modnDmr. reflexivity. } have -> : (modn (muln (@nat_of_ord (S (S (Zp_trunc q))) (@GRing.inv (FinRing.UnitRing.unitRingType (Zp_finUnitRingType (Zp_trunc q))) (@GRing.add (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q)))) (@otf Challenge s1) (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q)))) (@otf Challenge s2))))) (@nat_of_ord (S (S (Zp_trunc q))) (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2))))) q) = (Zp_mul (@GRing.inv (FinRing.UnitRing.unitRingType (Zp_finUnitRingType (Zp_trunc q))) (@GRing.add (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q)))) (@otf Challenge s1) (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q)))) (@otf Challenge s2)))) (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))). { simpl. rewrite modnDmr. rewrite <- order_ge1 at 9. rewrite modnMmr. reflexivity. } rewrite Zp_mulVz. 1: cbn ; by rewrite eq_refl. rewrite -> order_ge1 at 1. apply otf_neq in Heqb. rewrite prime_coprime. 2: apply prime_order. rewrite gtnNdvd. - done. - rewrite lt0n. apply neq_pos. assumption. - destruct (otf s1 - otf s2) as [k Hk]. simpl. rewrite order_ge1 in Hk. apply Hk. 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) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude SigmaProtocol) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)